CIRCUM.XGP[F83,JMC]10 - www.SailDart.org

perm filename CIRCUM.XGP[F83,JMC]10 blob sn#762075 filedate 1984-07-16 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ β∧Applications of Circumscription to Formalizing Common Sense Knowledge

␈↓ α∧␈↓α␈↓ ∧wby John McCarthy, Stanford University






␈↓ α∧␈↓Abstract:␈α
We␈α
present␈α
a␈α
new␈α
and␈α
more␈αsymmetric␈α
version␈α
of␈α
the␈α
circumscription␈α
method␈α
of␈αnon-
␈↓ α∧␈↓monotonic␈α⊂reasoning␈α⊂first␈α⊂described␈α⊂in␈α⊂(McCarthy␈α⊂1980)␈α⊂and␈α⊂some␈α⊂applications␈α⊃to␈α⊂formalizing
␈↓ α∧␈↓common␈α∂sense␈α∞knowledge.␈α∂ The␈α∂applications␈α∞in␈α∂this␈α∞paper␈α∂are␈α∂mostly␈α∞based␈α∂on␈α∂minimizing␈α∞the
␈↓ α∧␈↓abnormality␈αof␈α
different␈αaspects␈α
of␈αvarious␈α
entities.␈α Included␈α
are␈αnon-monotonic␈α
treatments␈αof␈α
␈↓↓is-
␈↓ α∧␈↓↓a␈↓␈α∂hierarchies,␈α∂the␈α∂unique␈α∂names␈α∂hypothesis,␈α∞and␈α∂the␈α∂frame␈α∂problem.␈α∂ The␈α∂new␈α∞circumscription
␈↓ α∧␈↓may␈α∪be␈α∪called␈α∪␈↓↓formula␈α∪circumscription␈↓␈α∪to␈α∩distinguish␈α∪it␈α∪from␈α∪the␈α∪previously␈α∪defined␈α∩␈↓↓domain
␈↓ α∧␈↓↓circumscription␈↓␈α⊂and␈α∂␈↓↓predicate␈α⊂circumscription␈↓.␈α⊂ A␈α∂still␈α⊂more␈α∂general␈α⊂formalism␈α⊂called␈α∂␈↓↓prioritized
␈↓ α∧␈↓↓circumscription␈↓ is briefly explored.

␈↓ α∧␈↓␈↓ αTThis draft contains only a preliminary treatment of prioritized circumscription.






␈↓ α∧␈↓Descriptors: non-monotonic logic, common sense, artificial intelligence.





















␈↓ α∧␈↓This version of circum[f83,jmc] pubbed at 12:21 on July 16, 1984.
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u2


␈↓ α∧␈↓1. ␈↓αIntroduction and new definition of circumscription␈↓

␈↓ α∧␈↓␈↓ αT(McCarthy␈α∂1980)␈α∞introduces␈α∂the␈α∞circumscription␈α∂method␈α∞of␈α∂non-monotonic␈α∂reasoning␈α∞and

␈↓ α∧␈↓gives␈αmotivation,␈αsome␈αmathematical␈αproperties␈αand␈αsome␈αexamples␈αof␈αits␈αapplication.␈α
 While␈αthe

␈↓ α∧␈↓present␈α⊃paper␈α⊃is␈α∩logically␈α⊃self-contained,␈α⊃motivation␈α⊃may␈α∩require␈α⊃some␈α⊃acquaintance␈α∩with␈α⊃the

␈↓ α∧␈↓earlier␈αpaper.␈α
 In␈αparticular␈α
we␈αdon't␈α
repeat␈αits␈α
arguments␈αabout␈α
the␈αimportance␈αof␈α
non-monotonic

␈↓ α∧␈↓reasoning in AI.  Also its examples are instructive.

␈↓ α∧␈↓␈↓ αTHere␈αwe␈αgive␈αa␈αmore␈αsymmetric␈α
definition␈αof␈αcircumscription␈αand␈αapplications␈αto␈αthe␈α
formal

␈↓ α∧␈↓expression␈αof␈αcommon␈αsense␈αfacts.␈α Our␈αlong␈αterm␈αgoal␈α(far␈αfrom␈αrealized␈αin␈αthe␈αpresent␈αpaper)␈αis

␈↓ α∧␈↓to␈αexpress␈αthese␈αfacts␈αin␈αa␈αway␈αthat␈αwould␈αbe␈αsuitable␈αfor␈αinclusion␈αin␈αa␈αgeneral␈αpurpose␈αdatabase

␈↓ α∧␈↓of␈α
common␈α∞sense␈α
facts.␈α
 We␈α∞imagine␈α
this␈α∞database␈α
to␈α
be␈α∞used␈α
by␈α
AI␈α∞programs␈α
written␈α∞after␈α
the

␈↓ α∧␈↓initial␈αpreparation␈αof␈αthe␈αdatabase.␈α It␈αwould␈αbe␈αbest␈αif␈αthe␈αwriters␈αof␈αthese␈αprograms␈αdidn't␈αhave

␈↓ α∧␈↓to␈α
be␈αfamiliar␈α
with␈α
how␈αthe␈α
common␈α
sense␈αfacts␈α
about␈α
particular␈αphenomena␈α
are␈αexpressed.␈α
 Thus

␈↓ α∧␈↓common␈α∩sense␈α∩knowledge␈α∩must␈α∪be␈α∩represented␈α∩in␈α∩a␈α∩way␈α∪that␈α∩is␈α∩not␈α∩specific␈α∩to␈α∪a␈α∩particular

␈↓ α∧␈↓application.

␈↓ α∧␈↓␈↓ αTIt␈α∞turns␈α
out␈α∞that␈α
many␈α∞such␈α
common␈α∞sense␈α∞facts␈α
can␈α∞be␈α
formalized␈α∞in␈α
a␈α∞uniform␈α∞way.␈α
 A

␈↓ α∧␈↓single␈α∞predicate␈α∞␈↓↓ab,␈↓␈α∞standing␈α∞for␈α∞"abnormal"␈α∞is␈α∞circumscribed␈α∞with␈α∞certain␈α∞other␈α∞predicates␈α∞and

␈↓ α∧␈↓functions␈αconsidered␈αas␈α
variables␈αthat␈αcan␈α
be␈αconstrained␈αto␈α
achieve␈αthe␈αcircumscription␈αsubject␈α
to

␈↓ α∧␈↓the␈αaxioms.␈α So␈α
far␈αthis␈αseems␈αto␈α
cover␈αthe␈αuse␈αof␈α
circumscription␈αto␈αrepresent␈αdefault␈α
rules.␈α On

␈↓ α∧␈↓the␈αother␈αhand,␈αit␈αdoesn't␈αseem␈αthat␈αcircumscribing␈αabnormality␈αcan␈αbe␈αused␈αto␈αcover␈αmany␈αof␈αthe

␈↓ α∧␈↓examples␈α⊂of␈α⊂(McCarthy␈α⊂1980)␈α⊃in␈α⊂which␈α⊂we␈α⊂want␈α⊃to␈α⊂limit␈α⊂a␈α⊂set␈α⊃to␈α⊂those␈α⊂objects␈α⊂that␈α⊃must␈α⊂be

␈↓ α∧␈↓members.


␈↓ α∧␈↓2. ␈↓αA new version of circumscription.␈↓


␈↓ α∧␈↓␈↓αDefinition:␈↓␈αLet␈α
␈↓↓A(P)␈↓␈αbe␈αa␈α
formula␈αof␈αsecond␈α
order␈αlogic,␈α
where␈α␈↓↓P␈↓␈αis␈α
a␈αtuple␈αof␈α
some␈αof␈α
the␈αfree


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u3


␈↓ α∧␈↓predicate␈αsymbols␈αin␈α␈↓↓A(P).␈↓␈α
Let␈α␈↓↓E(P,x)␈↓␈αbe␈αa␈αwff␈α
in␈αwhich␈α␈↓↓P␈↓␈αand␈α
a␈αtuple␈α␈↓↓x␈↓␈αof␈αindividual␈α
variables

␈↓ α∧␈↓occur free.  The circumscription of ␈↓↓E(P,x)␈↓ relative to ␈↓↓A(P)␈↓ is the formula ␈↓↓A'(P)␈↓ defined by

␈↓ α∧␈↓1)␈↓ αt ␈↓↓A(P) ∧ ∀P'.[A(P') ∧ [∀x.E(P',x) ⊃ E(P,x)] ⊃ [∀x.E(P',x) ≡ E(P,x)]].␈↓

␈↓ α∧␈↓[We␈α⊃are␈α⊃here␈α⊃writing␈α⊃␈↓↓A(P)␈↓␈α⊃instead␈α⊂of␈α⊃␈↓↓A(P␈↓β1␈↓↓,...,P␈↓βn␈↓↓)␈↓␈α⊃for␈α⊃brevity␈α⊃and␈α⊃likewise␈α⊃writing␈α⊂␈↓↓E(P,x)␈↓

␈↓ α∧␈↓instead␈αof␈α␈↓↓E(P␈↓β1␈↓↓,...,P␈↓βn␈↓↓,x␈↓β1␈↓↓,...,x␈↓βm␈↓↓)␈↓.␈α
 Likewise␈αthe␈αquantifier␈α␈↓↓∀x␈↓␈α
stands␈αfor␈α␈↓↓∀x␈↓β1␈↓↓...x␈↓βm␈↓↓␈↓.␈α In␈α
principle

␈↓ α∧␈↓␈↓↓A(P)␈↓␈α∞may␈α∞have␈α∞embedded␈α∞quantifiers,␈α∞but␈α∞we␈α∞have␈α∞no␈α∞applications␈α∞yet␈α∞that␈α∞use␈α∞this␈α
generality.

␈↓ α∧␈↓Circumscription␈α
is␈α
a␈α
kind␈α
of␈αminimization,␈α
and␈α
the␈α
predicate␈α
symbols␈αin␈α
␈↓↓A(P)␈↓␈α
that␈α
are␈α
not␈α
in␈α␈↓↓P␈↓

␈↓ α∧␈↓itself␈αact␈αas␈αparameters␈αin␈αthis␈αminimization.␈α When␈αwe␈αwish␈αto␈αmention␈αthese␈αother␈αpredicates␈α
we

␈↓ α∧␈↓will␈αwrite␈α␈↓↓A(P;Q)␈↓␈αand␈α␈↓↓E(P;Q,x)␈↓␈αwhere␈α␈↓↓Q␈↓␈αis␈αa␈αvector␈αof␈αpredicate␈αsymbols␈αwhich␈αare␈αnot␈αallowed␈α
to

␈↓ α∧␈↓be varied.


␈↓ α∧␈↓␈↓ αTThere␈α
are␈αtwo␈α
differences␈α
between␈αthis␈α
and␈α(McCarthy␈α
1980).␈α
 First,␈αin␈α
that␈α
paper␈α␈↓↓E(P,x)␈↓

␈↓ α∧␈↓had␈αthe␈α
specific␈αform␈α␈↓↓P(x).␈↓␈α
Here␈αwe␈α
speak␈αof␈αcircumscribing␈α
a␈αwff␈αand␈α
call␈αthe␈α
method␈α␈↓↓formula

␈↓ α∧␈↓↓circumscription␈↓,␈α
while␈α
there␈α
we␈α
could␈α
speak␈α
of␈αcircumscribing␈α
a␈α
predicate.␈α
 We␈α
can␈α
still␈α
speak␈αof

␈↓ α∧␈↓circumscribing␈αthe␈αpredicate␈α␈↓↓P␈↓␈αwhen␈α
␈↓↓E(P,x)␈↓␈αhas␈αthe␈αspecial␈αform␈α␈↓↓P(x).␈↓␈α
Formula␈αcircumscription

␈↓ α∧␈↓is␈α
more␈αsymmetric␈α
in␈αthat␈α
all␈αof␈α
the␈αpredicate␈α
symbols␈αin␈α
␈↓↓P␈↓␈αare␈α
regarded␈αas␈α
variables,␈αand␈α
a␈αwff␈α
is

␈↓ α∧␈↓minimized,␈α→whereas␈α→the␈α_earlier␈α→form␈α→distinguishes␈α→one␈α_of␈α→the␈α→predicates␈α→themselves␈α_for

␈↓ α∧␈↓minimization.  However, formula circumscription is reducible to predicate circumscription.

␈↓ α∧␈↓␈↓ αTSecond,␈α∩in␈α∩(1)␈α∩we␈α⊃use␈α∩an␈α∩explicit␈α∩quantifier␈α∩for␈α⊃the␈α∩predicate␈α∩variable␈α∩␈↓↓P'␈↓␈α∩whereas␈α⊃in

␈↓ α∧␈↓(McCarthy␈α
1980),␈α
the␈α
formula␈α
was␈α
a␈α
schema.␈α One␈α
advantage␈α
of␈α
the␈α
present␈α
formalism␈α
is␈αthat␈α
now

␈↓ α∧␈↓␈↓↓A'(P)␈↓␈α∀is␈α∃the␈α∀same␈α∀kind␈α∃of␈α∀formula␈α∃as␈α∀␈↓↓A(P)␈↓␈α∀and␈α∃can␈α∀be␈α∃used␈α∀as␈α∀part␈α∃of␈α∀the␈α∃axiom␈α∀for

␈↓ α∧␈↓circumscribing some other wff.

␈↓ α∧␈↓Remark:␈αThe␈αpredicate␈αsymbols␈α␈↓↓P␈↓β1␈↓↓,...,P␈↓βn␈↓↓␈↓␈αwill␈αnot␈αusually␈αbe␈αall␈αthe␈αpredicate␈αsymbols␈αoccurring

␈↓ α∧␈↓in␈α∀␈↓↓A(P).␈↓␈α∪The␈α∀situation␈α∪is␈α∀analogous␈α∀to␈α∪a␈α∀minimization␈α∪problem␈α∀in␈α∪calculus␈α∀or␈α∀calculus␈α∪of

␈↓ α∧␈↓variations.␈α
 Some␈α
quantity␈α
is␈αbeing␈α
minimized.␈α
 Other␈α
quantities␈αare␈α
variables␈α
whose␈α
values␈αare␈α
to

␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u4


␈↓ α∧␈↓be␈αchosen␈αso␈αas␈αto␈αachieve␈αthe␈αminimum.␈α Still␈αothers␈αare␈αparameters.␈α They␈αare␈αnot␈αvaried␈αin␈αthe

␈↓ α∧␈↓minimization␈α⊂process,␈α⊂and␈α⊂therefore␈α⊂the␈α⊂minimum␈α∂obtained␈α⊂and␈α⊂the␈α⊂values␈α⊂of␈α⊂the␈α∂minimizing

␈↓ α∧␈↓variables␈α⊃depend␈α⊂on␈α⊃the␈α⊃values␈α⊂of␈α⊃the␈α⊂parameters.␈α⊃ We␈α⊃will␈α⊂point␈α⊃out␈α⊂the␈α⊃variables␈α⊃and␈α⊂the

␈↓ α∧␈↓parameters␈αin␈α
the␈αsubsequent␈αexamples.␈α
 When␈αwe␈αwant␈α
to␈αbe␈αemphatic␈α
we␈αwill␈α
write␈α␈↓↓A(P;Q,x),␈↓

␈↓ α∧␈↓where the ␈↓↓P␈↓ are variable and the ␈↓↓Q␈↓ are parameters.

␈↓ α∧␈↓␈↓ αTIn␈α⊃some␈α⊃of␈α⊃the␈α⊃literature,␈α⊃it␈α⊂has␈α⊃been␈α⊃supposed␈α⊃that␈α⊃non-monotonic␈α⊃reasoning␈α⊂involves

␈↓ α∧␈↓giving␈α⊂all␈α∂predicates␈α⊂their␈α∂minimum␈α⊂extension.␈α∂ This␈α⊂mistake␈α∂has␈α⊂led␈α∂to␈α⊂theorems␈α⊂about␈α∂what

␈↓ α∧␈↓reasoning␈α
cannot␈αbe␈α
done␈αthat␈α
are␈α
irrelevant␈αto␈α
AI␈αand␈α
database␈αtheory,␈α
because␈α
their␈αpremisses

␈↓ α∧␈↓are too narrow.



␈↓ α∧␈↓3. ␈↓αA typology of uses of non-monotonic reasoning␈↓

␈↓ α∧␈↓␈↓ αTEach␈α∞of␈α∞the␈α∂several␈α∞papers␈α∞that␈α∂introduces␈α∞a␈α∞mode␈α∂of␈α∞non-monotonic␈α∞reasoning␈α∂seems␈α∞to

␈↓ α∧␈↓have␈αa␈αparticular␈αapplication␈αin␈αmind.␈α Perhaps␈αwe␈αare␈αlooking␈αat␈αdifferent␈αparts␈αof␈αan␈αelephant.

␈↓ α∧␈↓Therefore,␈α∞before␈α∞proceeding␈α∂to␈α∞applications␈α∞of␈α∂circumscription␈α∞I␈α∞want␈α∂to␈α∞suggest␈α∞a␈α∂typology␈α∞of

␈↓ α∧␈↓uses␈α
of␈α
non-monotonic␈α
reasoning.␈α
 The␈α
orientation␈αis␈α
towards␈α
circumscription,␈α
but␈α
I␈α
suppose␈αthe

␈↓ α∧␈↓considerations apply to other formalisms as well.

␈↓ α∧␈↓Non-monotonic reasoning has several uses.

␈↓ α∧␈↓1.␈αAs␈αa␈αcommunication␈αconvention.␈α Suppose␈αA␈αtells␈αB␈αabout␈αa␈αsituation␈αinvolving␈αa␈αbird.␈α If␈αthe

␈↓ α∧␈↓bird␈αcannot␈αfly,␈αand␈αthis␈αis␈αrelevant,␈αthen␈αA␈αmust␈αsay␈αso.␈α Whereas␈αif␈αthe␈αbird␈αcan␈αfly,␈αthere␈αis␈αno

␈↓ α∧␈↓requirement␈α
to␈α
mention␈α
the␈α
fact.␈α
 For␈αexample,␈α
if␈α
I␈α
hire␈α
you␈α
to␈αbuild␈α
me␈α
a␈α
bird␈α
cage␈α
and␈αyou␈α
don't

␈↓ α∧␈↓put␈αa␈αtop␈αon␈αit,␈αI␈αcan␈αget␈αout␈αof␈αpaying␈αfor␈αit␈αeven␈αif␈αyou␈αtell␈αthe␈αjudge␈αthat␈αI␈αnever␈αsaid␈αmy␈αbird

␈↓ α∧␈↓could␈αfly.␈α However,␈α
if␈αI␈αcomplain␈αthat␈α
you␈αwasted␈αmoney␈α
by␈αputting␈αa␈αtop␈α
on␈αa␈αcage␈α
I␈αintended

␈↓ α∧␈↓for a penguin, the judge will agree with you that if the bird couldn't fly I should have said so.

␈↓ α∧␈↓2.␈α⊂As␈α⊂a␈α⊃database␈α⊂or␈α⊂information␈α⊂storage␈α⊃convention.␈α⊂ It␈α⊂may␈α⊂be␈α⊃a␈α⊂convention␈α⊂of␈α⊃a␈α⊂particular


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u5


␈↓ α∧␈↓database␈αthat␈αcertain␈αpredicates␈αhave␈α
their␈αminimal␈αextension.␈α This␈αgeneralizes␈αthe␈α
closed␈αworld

␈↓ α∧␈↓assumption.␈α∀ When␈α∃a␈α∀database␈α∀makes␈α∃the␈α∀closed␈α∃world␈α∀assumption␈α∀for␈α∃all␈α∀predicates␈α∃it␈α∀is

␈↓ α∧␈↓reasonable␈α
to␈α
imbed␈αthis␈α
fact␈α
in␈α
the␈αprograms␈α
that␈α
use␈α
the␈αdatabase.␈α
 However,␈α
when␈α
only␈αsome

␈↓ α∧␈↓predicates␈α⊃are␈α∩to␈α⊃be␈α∩minimized,␈α⊃we␈α⊃need␈α∩to␈α⊃say␈α∩which␈α⊃ones␈α⊃by␈α∩appropriate␈α⊃sentences␈α∩of␈α⊃the

␈↓ α∧␈↓database,␈α
perhaps␈α
as␈α
a␈α
preamble␈α
to␈α
the␈αcollection␈α
of␈α
ground␈α
sentences␈α
that␈α
usually␈α
constitute␈αthe

␈↓ α∧␈↓main content.

␈↓ α∧␈↓␈↓ αTNeither␈α1␈α
nor␈α2␈αrequires␈α
that␈αmost␈αbirds␈α
can␈αfly.␈α Should␈α
it␈αhappen␈αthat␈α
most␈αbirds␈αthat␈α
are

␈↓ α∧␈↓subject␈αto␈αthe␈αcommunication␈αor␈αabout␈αwhich␈αinformation␈αis␈αrequested␈αfrom␈αthe␈αdata␈αbase␈αcannot

␈↓ α∧␈↓fly, the convention may lead to inefficiency but not incorrectness.

␈↓ α∧␈↓3.␈αAs␈α
a␈αrule␈α
of␈αconjecture.␈α
 This␈αuse␈αwas␈α
emphasized␈αin␈α
(McCarthy␈α1980).␈α
 The␈αcircumscriptions

␈↓ α∧␈↓may␈αbe␈αregarded␈αas␈αexpressions␈αof␈αsome␈αprobabilistic␈αnotions␈αsuch␈αas␈α"most␈αbirds␈αcan␈αfly"␈αor␈αthey

␈↓ α∧␈↓may␈αbe␈α
expressions␈αof␈αstandard␈α
cases.␈α Thus␈α
it␈αis␈αsimple␈α
to␈αconjecture␈αthat␈α
there␈αare␈α
no␈αrelevant

␈↓ α∧␈↓present␈α⊂material␈α⊂objects␈α⊂other␈α⊂than␈α∂those␈α⊂whose␈α⊂presence␈α⊂can␈α⊂be␈α∂inferred.␈α⊂ It␈α⊂is␈α⊂also␈α⊂a␈α∂simple

␈↓ α∧␈↓conjecture␈α
that␈α∞a␈α
tool␈α∞asserted␈α
to␈α
be␈α∞present␈α
is␈α∞usable␈α
for␈α
its␈α∞normal␈α
function.␈α∞ Such␈α
conjectures

␈↓ α∧␈↓sometimes␈α∂conflict,␈α⊂but␈α∂there␈α∂is␈α⊂nothing␈α∂wrong␈α∂with␈α⊂having␈α∂incompatible␈α∂conjectures␈α⊂on␈α∂hand.

␈↓ α∧␈↓Besides␈α
the␈αpossibility␈α
of␈αdeciding␈α
that␈αone␈α
is␈αcorrect␈α
and␈α
the␈αother␈α
wrong,␈αit␈α
is␈αpossible␈α
to␈αuse␈α
one

␈↓ α∧␈↓for generating possible exceptions to the other.

␈↓ α∧␈↓4.␈α
As␈α
a␈αrepresentation␈α
of␈α
a␈αpolicy.␈α
 The␈α
example␈αis␈α
Doyle's␈α
"The␈αmeeting␈α
will␈α
be␈α
on␈αWednesday

␈↓ α∧␈↓unless another decision is explicitly made".  Again probabilities are not involved.

␈↓ α∧␈↓5.␈α∂As␈α∂a␈α⊂very␈α∂streamlined␈α∂expression␈α∂of␈α⊂probabilistic␈α∂information␈α∂when␈α⊂numerical␈α∂probabilities,

␈↓ α∧␈↓especially␈α⊗conditional␈α∃probabilities,␈α⊗are␈α∃unobtainable.␈α⊗ Since␈α∃circumscription␈α⊗doesn't␈α∃provide

␈↓ α∧␈↓numerical␈α∃probabilities,␈α∃its␈α∃probabilistic␈α∃interpretation␈α∃involves␈α∃probabilities␈α∃that␈α∃are␈α∀either

␈↓ α∧␈↓infinitesimal,␈αwithin␈αan␈αinfinitesimal␈αof␈αone,␈αor␈αintermediate␈α-␈αwithout␈αany␈αdiscrimination␈αamong

␈↓ α∧␈↓the␈αintermediate␈αvalues.␈α The␈αcircumscriptions␈αgive␈αconditional␈αprobabilities.␈α Thus␈αwe␈α
may␈αtreat


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u6


␈↓ α∧␈↓the␈α
probability␈αthat␈α
a␈αbird␈α
can't␈α
fly␈αas␈α
an␈αinfinitesimal.␈α
 However,␈α
if␈αthe␈α
rare␈αevent␈α
occurs␈αthat␈α
the

␈↓ α∧␈↓bird␈α
is␈αa␈α
penguin,␈α
then␈αthe␈α
conditional␈α
probability␈αthat␈α
it␈α
can␈αfly␈α
is␈α
infinitesimal,␈αbut␈α
we␈αmay␈α
hear

␈↓ α∧␈↓of some rare condition that would allow it to fly after all.

␈↓ α∧␈↓␈↓ αTWhy␈αdon't␈α
we␈αuse␈α
finite␈αprobabilities␈α
combined␈αby␈α
the␈αusual␈α
laws?␈α That␈α
would␈αbe␈α
fine␈αif

␈↓ α∧␈↓we␈α
had␈α
the␈α
numbers,␈α
but␈α
circumscription␈α
is␈α
usable␈αwhen␈α
we␈α
can't␈α
get␈α
the␈α
numbers␈α
or␈α
find␈αtheir

␈↓ α∧␈↓use␈αinconvenient.␈α Note␈α
that␈αthe␈αgeneral␈αprobability␈α
that␈αa␈αbird␈αcan␈α
fly␈αmay␈αbe␈αirrelevant,␈α
because

␈↓ α∧␈↓we␈α
are␈α
interested␈α
in␈α
the␈α
facts␈α
that␈α
influence␈αour␈α
opinion␈α
about␈α
whether␈α
a␈α
particular␈α
bird␈α
can␈αfly␈α
in

␈↓ α∧␈↓a particular situation.

␈↓ α∧␈↓␈↓ αTMoreover,␈α⊂the␈α⊂use␈α⊂of␈α⊂probabilities␈α⊂is␈α⊂normally␈α⊂considered␈α⊂to␈α⊂require␈α⊂the␈α⊂definition␈α⊂of␈α∂a

␈↓ α∧␈↓sample␈α
space,␈α
i.e.␈α
the␈αspace␈α
of␈α
all␈α
possibilities.␈α
 Circumscription␈αallows␈α
one␈α
to␈α
conjecture␈α
that␈αthe

␈↓ α∧␈↓cases␈α
we␈α
know␈α
about␈α
are␈α
all␈α
that␈α
there␈α
are.␈α
 However,␈α
when␈α
additional␈α
cases␈α
are␈α
found,␈αthe␈α
axioms

␈↓ α∧␈↓don't have to be changed.  Thus there is no fixed space of all possibilities.

␈↓ α∧␈↓␈↓ αTNotice␈α∞also␈α
that␈α∞circumscription␈α
does␈α∞not␈α∞provide␈α
for␈α∞weighing␈α
evidence;␈α∞it␈α∞is␈α
appropriate

␈↓ α∧␈↓when␈αthe␈αinformation␈αpermits␈αsnap␈αdecisions.␈α However,␈αmany␈αcases␈αnominally␈αtreated␈αin␈αterms␈αof

␈↓ α∧␈↓weighing␈α∞information␈α∞are␈α∂in␈α∞fact␈α∞cases␈α∂in␈α∞which␈α∞the␈α∞weights␈α∂are␈α∞such␈α∞that␈α∂circumscription␈α∞and

␈↓ α∧␈↓other defaults work better.

␈↓ α∧␈↓6.␈αAuto-epistemic␈αreasoning.␈α "If␈αI␈α
had␈αan␈αelder␈αbrother,␈αI'd␈α
know␈αit".␈α This␈αhas␈αbeen␈α
studied␈αby

␈↓ α∧␈↓R. Moore.  Perhaps it can be handled by circumscription.

␈↓ α∧␈↓7.␈αBoth␈αcommon␈α
sense␈αphysics␈αand␈α
common␈αsense␈αpsychology␈α
use␈αnon-monotonic␈αrules.␈α An␈α
object

␈↓ α∧␈↓will␈α
continue␈αin␈α
a␈αstraight␈α
line␈α
if␈αnothing␈α
interferes␈αwith␈α
it.␈α
 A␈αperson␈α
will␈αeat␈α
when␈αhungry␈α
unless

␈↓ α∧␈↓something␈α∪prevents␈α∩it.␈α∪ Such␈α∪rules␈α∩are␈α∪open␈α∩ended␈α∪about␈α∪what␈α∩might␈α∪prevent␈α∪the␈α∩expected

␈↓ α∧␈↓behavior,␈α
and␈α
this␈α∞is␈α
required,␈α
because␈α
we␈α∞are␈α
always␈α
encountering␈α
unexpected␈α∞phenomena␈α
that

␈↓ α∧␈↓modify␈α∂the␈α∂operation␈α∂of␈α∂our␈α∂rules.␈α∂ Science,␈α∂as␈α∂distinct␈α∂from␈α∂common␈α∂sense,␈α∂tries␈α∂to␈α∂work␈α∞with

␈↓ α∧␈↓exceptionless␈α⊂rules.␈α⊂ However,␈α⊂this␈α⊂means␈α⊂that␈α⊂common␈α⊂sense␈α⊂reasoning␈α⊂has␈α⊂to␈α⊂decide␈α⊃when␈α⊂a


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u7


␈↓ α∧␈↓scientific␈α
model␈α
is␈αapplicable,␈α
i.e.␈α
that␈α
there␈αare␈α
no␈α
important␈αphenomena␈α
not␈α
taken␈α
into␈αaccount

␈↓ α∧␈↓by the theories being used and the model of the particular phenomena.

␈↓ α∧␈↓␈↓ αTSeven␈α∩different␈α∩uses␈α∩for␈α∩non-monotonic␈α∪reasoning␈α∩seem␈α∩too␈α∩many,␈α∩so␈α∩perhaps␈α∪we␈α∩can

␈↓ α∧␈↓condense later.



␈↓ α∧␈↓4. ␈↓αMinimizing abnormality␈↓

␈↓ α∧␈↓␈↓ αTMany␈α⊂people␈α⊂have␈α⊂proposed␈α⊂representing␈α⊂facts␈α⊂about␈α⊂what␈α⊂is␈α⊂"normally"␈α⊂the␈α⊂case.␈α⊂ One

␈↓ α∧␈↓problem␈αis␈αthat␈αevery␈αobject␈αis␈αabnormal␈αin␈αsome␈αway,␈αand␈αwe␈αwant␈αto␈αallow␈αsome␈αaspects␈αof␈αthe

␈↓ α∧␈↓object␈αto␈αbe␈αabnormal␈αand␈αstill␈αassume␈αthe␈αnormality␈αof␈αthe␈αrest.␈α We␈αdo␈αthis␈αwith␈αa␈αpredicate␈α␈↓↓ab␈↓

␈↓ α∧␈↓standing␈α
for␈α
"abnormal".␈α We␈α
circumscribe␈α
␈↓↓ab z␈↓.␈α The␈α
argument␈α
of␈α␈↓↓ab␈↓␈α
will␈α
be␈αsome␈α
aspect␈α
of␈αthe

␈↓ α∧␈↓entities␈α
involved.␈α Some␈α
aspects␈α
can␈αbe␈α
abnormal␈α
without␈αaffecting␈α
others.␈α
 The␈αaspects␈α
themselves

␈↓ α∧␈↓are abstract entities, and their unintuitiveness is somewhat a blemish on the theory.

␈↓ α∧␈↓␈↓ αTThere are many applications.



␈↓ α∧␈↓5. ␈↓αWhether birds can fly␈↓

␈↓ α∧␈↓␈↓ αTMarvin␈α~Minsky␈α~(1982)␈α~offered␈α~expressing␈α~the␈α~facts␈α~and␈α~non-monotonic␈α→reasoning

␈↓ α∧␈↓concerning␈α⊂the␈α⊂ability␈α⊂of␈α⊂birds␈α⊂to␈α⊂fly␈α⊂as␈α∂a␈α⊂challenge␈α⊂to␈α⊂advocates␈α⊂of␈α⊂formal␈α⊂systems␈α⊂based␈α∂on

␈↓ α∧␈↓mathematical logic.

␈↓ α∧␈↓␈↓ αTThere␈α
are␈α
many␈α
ways␈α
of␈α
non-monotonically␈α
axiomatizing␈α
the␈α
facts␈α
about␈α
which␈α∞birds␈α
can

␈↓ α∧␈↓fly.  The following set of axioms using ␈↓↓ab␈↓ seems to me quite straightforward.

␈↓ α∧␈↓2)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓Unless␈αan␈αobject␈αis␈αabnormal␈αin␈α␈↓↓aspect1,␈↓␈αit␈αcan't␈αfly.␈α (We're␈αusing␈αa␈αconvention␈αthat␈αparentheses

␈↓ α∧␈↓may␈α∪be␈α∀omitted␈α∪for␈α∪functions␈α∀and␈α∪predicates␈α∀of␈α∪one␈α∪argument,␈α∀so␈α∪that␈α∪(2)␈α∀is␈α∪the␈α∀same␈α∪as

␈↓ α∧␈↓␈↓↓∀x.(¬ab(aspect1(x) ⊃ ¬flies(x))␈↓.)


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u8


␈↓ α∧␈↓␈↓ αTNote␈α
that␈α
it␈α
wouldn't␈α
work␈α
to␈α
write␈α
␈↓↓ab␈α
x␈↓␈α
instead␈α
of␈α
␈↓↓ab␈α
aspect1␈α
x␈↓,␈α
because␈α
we␈α
don't␈α∞want␈α
a

␈↓ α∧␈↓bird␈α⊂that␈α⊂is␈α⊂abnormal␈α⊂with␈α⊂respect␈α⊂to␈α⊂its␈α⊂ability␈α⊂to␈α⊂fly␈α⊂to␈α⊂be␈α⊂automatically␈α⊂abnormal␈α⊂in␈α⊂other

␈↓ α∧␈↓respects.  Using aspects limits the effects of proofs of abnormality.

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀x.bird x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓A␈αbird␈αis␈αabnormal␈αin␈α
␈↓↓aspect1,␈↓␈αso␈α(2)␈αcan't␈αbe␈α
used␈αto␈αshow␈αit␈αcan't␈α
fly.␈α If␈α(3)␈αwere␈αomitted,␈α
when

␈↓ α∧␈↓we␈α∩did␈α∩the␈α∩circumscription␈α∩we␈α⊃would␈α∩only␈α∩be␈α∩able␈α∩to␈α⊃infer␈α∩a␈α∩disjunction.␈α∩ Either␈α∩a␈α∩bird␈α⊃is

␈↓ α∧␈↓abnormal␈α∞in␈α
␈↓↓aspect1␈↓␈α∞or␈α
it␈α∞can␈α
fly␈α∞unless␈α
it␈α∞is␈α
abnormal␈α∞in␈α
␈↓↓aspect2.␈↓␈α∞(3)␈α
establishes␈α∞expresses␈α
our

␈↓ α∧␈↓preference␈α∂for␈α∞inferring␈α∂that␈α∞a␈α∂bird␈α∞is␈α∂abnormal␈α∞in␈α∂␈↓↓aspect1␈↓␈α∞rather␈α∂than␈α∞␈↓↓aspect2.␈↓␈α∂We␈α∞call␈α∂(3)␈α∞a

␈↓ α∧␈↓␈↓↓cancellation of inheritance␈↓ axiom.  We will see more of them.

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.

␈↓ α∧␈↓Unless a bird is abnormal in ␈↓↓aspect2,␈↓ it can fly.

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓Ostriches␈α
are␈α
abnormal␈α
in␈α
␈↓↓aspect2.␈↓␈α
This␈α
doesn't␈α
say␈αthat␈α
an␈α
ostrich␈α
cannot␈α
fly␈α
-␈α
merely␈α
that␈α(4)

␈↓ α∧␈↓can't be used to infer that it does.  (5) is another cancellation of inheritance axiom.

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀x.penguin x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓Penguins are also abnormal in ␈↓↓aspect2.␈↓

␈↓ α∧␈↓7)␈↓ αt ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓8)␈↓ αt ␈↓↓∀x.penguin x ∧¬ab aspect4 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓Normally␈α∞ostriches␈α∂and␈α∞penguins␈α∞can't␈α∂fly.␈α∞ However,␈α∞there␈α∂is␈α∞an␈α∞out.␈α∂ (7)␈α∞and␈α∞(8)␈α∂provide␈α∞that

␈↓ α∧␈↓under␈α⊃unspecified␈α⊃conditions,␈α⊃an␈α⊃ostrich␈α⊃or␈α⊃penguin␈α⊃might␈α⊃fly␈α⊃after␈α⊃all.␈α⊃ If␈α⊃we␈α⊃give␈α∩no␈α⊃such

␈↓ α∧␈↓conditions,␈αwe␈α
will␈αconclude␈α
that␈αan␈α
ostrich␈αor␈α
penguin␈αcan't␈α
fly.␈α Additional␈α
objects␈αthat␈α
can␈αfly

␈↓ α∧␈↓may␈α∂be␈α∂specified.␈α⊂ Each␈α∂needs␈α∂two␈α∂axioms.␈α⊂ The␈α∂first␈α∂says␈α∂that␈α⊂it␈α∂is␈α∂abnormal␈α∂in␈α⊂␈↓↓aspect1␈↓␈α∂and

␈↓ α∧␈↓prevents␈α(2)␈αfrom␈αbeing␈αused␈αto␈αsay␈αthat␈αit␈αcan't␈αfly.␈α The␈αsecond␈αprovides␈αthat␈αit␈αcan␈αfly␈αunless␈αit

␈↓ α∧␈↓is␈α
abnormal␈αin␈α
yet␈αanother␈α
way.␈α
 Additional␈αnon-flying␈α
birds␈αcan␈α
also␈α
be␈αprovided␈α
for␈αat␈α
a␈αcost␈α
of

␈↓ α∧␈↓two axioms per kind.
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ u9


␈↓ α∧␈↓␈↓ αTWe␈α
haven't␈αyet␈α
said␈αthat␈α
ostriches␈αand␈α
penguins␈αare␈α
birds,␈αso␈α
let's␈αdo␈α
that␈αand␈α
throw␈αin␈α
that

␈↓ α∧␈↓canaries are birds also.

␈↓ α∧␈↓9)␈↓ αt ␈↓↓∀x.ostrich x ⊃ bird x␈↓

␈↓ α∧␈↓10)␈↓ αt ␈↓↓∀x.penguin x ⊃ bird x␈↓

␈↓ α∧␈↓11)␈↓ αt ␈↓↓∀x.canary x ∧ ¬ab aspect5 x ⊃ bird x␈↓.

␈↓ α∧␈↓We␈α∂threw␈α∂in␈α⊂␈↓↓aspect5␈↓␈α∂just␈α∂in␈α⊂case␈α∂one␈α∂wanted␈α⊂to␈α∂use␈α∂the␈α⊂term␈α∂canary␈α∂in␈α⊂the␈α∂sense␈α∂of␈α⊂a␈α∂1930s

␈↓ α∧␈↓gangster movie.

␈↓ α∧␈↓Asserting␈α
that␈α
ostriches,␈α
penguins␈α
and␈α
canaries␈α∞are␈α
birds␈α
will␈α
help␈α
inherit␈α
other␈α∞properties␈α
from

␈↓ α∧␈↓the class of birds.  For example, we have

␈↓ α∧␈↓12)␈↓ αt ␈↓↓∀x. bird x ∧ ¬ab aspect6 x ⊃ feathered x␈↓.

␈↓ α∧␈↓So␈αfar␈αthere␈α
is␈αnothing␈αto␈α
prevent␈αostriches,␈αpenguins␈αand␈α
canaries␈αfrom␈αoverlapping.␈α
 We␈αcould

␈↓ α∧␈↓write disjointness axioms like

␈↓ α∧␈↓13)␈↓ αt␈↓↓∀x. ¬ostrich x ∨ ¬penguin x␈↓,

␈↓ α∧␈↓but we require ␈↓↓n␈↓∧2␈↓ of them if we have ␈↓↓n␈↓ species.  It is more efficient to write axioms like

␈↓ α∧␈↓14)␈↓ αt␈↓↓∀x.ostrich x ⊃ species x = 'ostrich␈↓,

␈↓ α∧␈↓which␈α
makes␈α
the␈α
␈↓↓n␈↓␈α
species␈α
disjoint␈α
with␈αonly␈α
␈↓↓n␈↓␈α
axioms␈α
assuming␈α
that␈α
the␈α
distinctness␈α
of␈αthe␈α
names

␈↓ α∧␈↓is apparent to the reasoner.  This problem is like the unique names problem.

␈↓ α∧␈↓␈↓ αTIf␈αthese␈αare␈αthe␈αonly␈αfacts␈αto␈αbe␈αtaken␈αinto␈αaccount,␈αwe␈αmust␈αsomehow␈αspecify␈αthat␈αwhat␈αcan

␈↓ α∧␈↓fly␈α⊂is␈α⊂to␈α⊂be␈α⊂determined␈α⊂by␈α⊂circumscribing␈α⊂the␈α⊂wff␈α⊂␈↓↓ab z␈↓␈α⊂using␈α⊂␈↓↓ab␈↓␈α⊂and␈α⊂␈↓↓flies␈↓␈α⊂as␈α⊂variables.␈α⊂ Why

␈↓ α∧␈↓exactly␈α
these?␈α∞ If␈α
␈↓↓ab␈↓␈α∞were␈α
not␈α∞taken␈α
as␈α∞variable,␈α
␈↓↓ab z␈↓␈α∞couldn't␈α
vary␈α∞either,␈α
and␈α∞the␈α
minimization

␈↓ α∧␈↓problem␈α
would␈α
go␈α
away.␈α
 Since␈α
the␈α
purpose␈α
of␈α
the␈α
axiom␈α
set␈α
is␈α
to␈α
describe␈α
what␈α
flies,␈α
the␈α
predicate

␈↓ α∧␈↓␈↓↓flies␈↓␈αmust␈αbe␈αvaried␈αalso.␈α Suppose␈αwe␈αcontemplate␈αtaking␈α␈↓↓bird␈↓␈αas␈αvariable␈αalso.␈α In␈αthe␈αfirst␈αplace,

␈↓ α∧␈↓this␈αviolates␈αan␈αintuition␈αthat␈αdeciding␈αwhat␈α
flies␈αfollows␈αdeciding␈αwhat␈αis␈αa␈αbird␈αin␈α
the␈αcommon

␈↓ α∧␈↓sense␈α
situations␈α
we␈α
want␈αto␈α
cover.␈α
 Secondly,␈α
if␈αwe␈α
use␈α
exactly␈α
the␈αabove␈α
axioms␈α
and␈α
admit␈αbird␈α
as


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f10


␈↓ α∧␈↓a␈α⊂variable,␈α⊂we␈α⊃will␈α⊂further␈α⊂conclude␈α⊃that␈α⊂the␈α⊂only␈α⊂birds␈α⊃are␈α⊂penguins,␈α⊂canaries␈α⊃and␈α⊂ostriches.

␈↓ α∧␈↓Namely,␈α⊃for␈α⊃these␈α⊃entities␈α⊃something␈α⊃has␈α⊂to␈α⊃be␈α⊃abnormal,␈α⊃and␈α⊃therefore␈α⊃minimizing␈α⊃␈↓↓ab z␈↓␈α⊂will

␈↓ α∧␈↓involve␈α⊂making␈α⊂as␈α∂few␈α⊂entities␈α⊂as␈α⊂possible␈α∂penguins,␈α⊂canaries␈α⊂and␈α∂ostriches.␈α⊂ If␈α⊂we␈α⊂also␈α∂admit

␈↓ α∧␈↓␈↓↓penguin,␈↓␈α␈↓↓ostrich,␈↓␈αand␈α␈↓↓canary␈↓␈αas␈αvariable,␈αwe␈αwill␈αsucceed␈αin␈αmaking␈α␈↓↓ab z␈↓␈αalways␈αfalse,␈αand␈αthere

␈↓ α∧␈↓will be no birds at all.

␈↓ α∧␈↓␈↓ αTHowever,␈α
if␈αthe␈α
same␈α
circumscriptions␈αare␈α
done␈α
with␈αadditional␈α
axioms␈α
like␈α␈↓↓canary Tweety␈↓

␈↓ α∧␈↓and␈α␈↓↓ostrich Joe,␈↓␈α
we␈αwill␈α
get␈αthe␈α
expected␈αresult␈αthat␈α
Tweety␈αcan␈α
fly␈αand␈α
Joe␈αcannot␈α
even␈αif␈αall␈α
the

␈↓ α∧␈↓above are variable.

␈↓ α∧␈↓␈↓ αTWhile␈α∩this␈α∩works␈α∩it␈α∩may␈α∩be␈α∩more␈α⊃straightforward,␈α∩and␈α∩therefore␈α∩less␈α∩likely␈α∩to␈α∩lead␈α⊃to

␈↓ α∧␈↓subsequent trouble, to circumscribe birds, ostriches and penguins with axioms like

␈↓ α∧␈↓15)␈↓ αt ␈↓↓∀x.¬ab aspect8 x ⊃ ¬bird x␈↓, etc.

␈↓ α∧␈↓␈↓ αTWe␈αhave␈αnot␈αyet␈αspecified␈αhow␈αa␈αprogram␈αwill␈αknow␈αwhat␈αto␈αcircumscribe.␈α One␈αextreme␈αis

␈↓ α∧␈↓to␈α
build␈αit␈α
into␈αthe␈α
program,␈αbut␈α
this␈αis␈α
contrary␈αto␈α
the␈αdeclarative␈α
spirit.␈α However,␈α
a␈αstatement␈α
of

␈↓ α∧␈↓what␈αto␈αcircumscribe␈αisn't␈αjust␈αa␈αsentence␈αof␈αthe␈αlanguage␈αbecause␈αof␈αits␈αnon-monotonic␈αcharacter.

␈↓ α∧␈↓My␈αpresent,␈αadmittedly␈αsomewhat␈αunsatisfactory,␈αidea␈αis␈αto␈αinclude␈αsome␈αsort␈αof␈αmetamathematical

␈↓ α∧␈↓statement like

␈↓ α∧␈↓16)␈↓ αt ␈↓↓circumsribe(ab z; ab, flies, bird, ostrich, penguin)␈↓

␈↓ α∧␈↓in␈α⊂a␈α⊂"policy"␈α⊂database␈α⊂available␈α⊃to␈α⊂the␈α⊂program.␈α⊂ (16)␈α⊂is␈α⊂intended␈α⊃to␈α⊂mean␈α⊂that␈α⊂␈↓↓ab z␈↓␈α⊂is␈α⊃to␈α⊂be

␈↓ α∧␈↓circumscribed␈α
with␈α
␈↓↓ab,␈↓␈α
␈↓↓flies,␈↓␈α
␈↓↓bird,␈↓␈α
␈↓↓ostrich␈↓␈α
and␈α
␈↓↓penguin␈↓␈α
taken␈α
as␈α
variable.␈α
 Explicitly␈α
listing␈α
the

␈↓ α∧␈↓variables␈α∪makes␈α∀adding␈α∪new␈α∪kinds␈α∀awkward,␈α∪since␈α∪they␈α∀will␈α∪have␈α∪to␈α∀be␈α∪mentioned␈α∀in␈α∪the

␈↓ α∧␈↓␈↓↓circumscribe␈↓ statement.


␈↓ α∧␈↓6. ␈↓αThe unique names hypothesis␈↓

␈↓ α∧␈↓␈↓ αTRaymond␈α↔Reiter␈α_(1980b)␈α↔introduced␈α_the␈α↔phrase␈α↔"unique␈α_names␈α↔hypothesis"␈α_for␈α↔the

␈↓ α∧␈↓assumption␈α
each␈α
object␈α
has␈α
a␈α
unique␈α
name,␈α
i.e.␈α
 that␈α
distinct␈α
names␈α
denote␈α
distinct␈α∞objects.␈α
 We

␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f11


␈↓ α∧␈↓want␈αto␈αtreat␈αthis␈αnon-monotonically.␈α Namely,␈αwe␈αwant␈αa␈αwff␈αthat␈αpicks␈αout␈αthose␈αmodels␈α
of␈αour

␈↓ α∧␈↓initial␈α
assumptions␈α
maximize␈αthe␈α
inequality␈α
of␈αthe␈α
denotations␈α
of␈αconstant␈α
symbols.␈α
 While␈αwe're

␈↓ α∧␈↓at␈α∂it,␈α∞we␈α∂might␈α∂as␈α∞well␈α∂try␈α∂for␈α∞something␈α∂stronger.␈α∂ We␈α∞want␈α∂to␈α∂maximize␈α∞the␈α∂extent␈α∂to␈α∞which

␈↓ α∧␈↓distinct␈α∩terms␈α∩designate␈α⊃distinct␈α∩objects.␈α∩ When␈α∩there␈α⊃is␈α∩a␈α∩unique␈α⊃model␈α∩of␈α∩the␈α∩axioms␈α⊃that

␈↓ α∧␈↓maximizes␈α∂distinctness,␈α∂we␈α∞can␈α∂put␈α∂it␈α∂more␈α∞simply;␈α∂two␈α∂terms␈α∞denote␈α∂distinct␈α∂objects␈α∂unless␈α∞the

␈↓ α∧␈↓axioms␈αforce␈αthem␈αto␈αdenote␈αthe␈αsame.␈α If␈αwe␈αare␈αeven␈αmore␈αfortunate,␈αas␈αwe␈αare␈αin␈αthe␈αexamples

␈↓ α∧␈↓to be given, we can say that two terms denote distinct objects unless their equality is provable.

␈↓ α∧␈↓␈↓ αTWe␈α∩don't␈α∩know␈α∩a␈α∩completely␈α∩satisfactory␈α∩way␈α⊃of␈α∩doing␈α∩this.␈α∩ Suppose␈α∩that␈α∩we␈α∩have␈α⊃a

␈↓ α∧␈↓language␈α∂␈↓↓L␈↓␈α∂and␈α∂a␈α∂theory␈α∂␈↓↓T␈↓␈α∂consisting␈α∂of␈α⊂the␈α∂consequences␈α∂of␈α∂a␈α∂formula␈α∂␈↓↓A.␈↓␈α∂It␈α∂would␈α⊂be␈α∂most

␈↓ α∧␈↓pleasant␈α
if␈α∞we␈α
could␈α
just␈α∞circumscribe␈α
equality,␈α
but␈α∞as␈α
Reiter␈α
and␈α∞Etherington␈α
(to␈α∞be␈α
published)

␈↓ α∧␈↓point␈α∂out,␈α∂this␈α∂doesn't␈α∂work,␈α∂and␈α∂nothing␈α∂similar␈α∂works.␈α∂ We␈α∂could␈α∂hope␈α∂to␈α∂circumscribe␈α∂some

␈↓ α∧␈↓other␈α∞formula␈α∞of␈α∞the␈α∞␈↓↓L,␈↓␈α∞but␈α∞this␈α∞doesn't␈α∞seem␈α∞to␈α∞work␈α∞either.␈α∞ Failing␈α∞that,␈α∞we␈α∞could␈α∂hope␈α∞for

␈↓ α∧␈↓some␈αother␈αsecond␈αorder␈αformula␈αtaken␈αfrom␈α␈↓↓L␈↓␈αthat␈αwould␈αexpress␈αthe␈αunique␈αnames␈αhypothesis,

␈↓ α∧␈↓but we don't presently see how to do it.

␈↓ α∧␈↓␈↓ αTOur␈α
solution␈α
involves␈αextending␈α
the␈α
language␈αby␈α
introducing␈α
the␈αnames␈α
themselves␈α
as␈αthe

␈↓ α∧␈↓only objects.  All assertions about objects are expressed as assertions about the names.

␈↓ α∧␈↓␈↓ αTWe␈αsuppose␈αour␈αtheory␈αis␈αsuch␈α
that␈αthe␈αnames␈αthemselves␈αare␈αall␈αprovably␈α
distinct.␈α There

␈↓ α∧␈↓are␈α
several␈α
ways␈α
of␈α
doing␈α
this.␈α
 Let␈α
the␈α
names␈αbe␈α
␈↓↓n1,␈↓␈α
␈↓↓n2,␈↓␈α
etc.␈α
 The␈α
simplest␈α
solution␈α
is␈α
to␈αhave␈α
an

␈↓ α∧␈↓axiom␈α␈↓↓ni ≠nj␈↓␈αfor␈αeach␈αpair␈αof␈αdistinct␈αnames.␈α This␈αrequires␈αa␈αnumber␈αof␈αaxioms␈αproportional␈αto

␈↓ α∧␈↓the␈α
square␈αof␈α
the␈α
number␈αof␈α
names,␈α
which␈αis␈α
sometimes␈α
objectionable.␈α The␈α
next␈αsolution␈α
involves

␈↓ α∧␈↓introducing␈α⊂an␈α⊂arbitrary␈α⊂ordering␈α∂on␈α⊂the␈α⊂names.␈α⊂ We␈α∂have␈α⊂special␈α⊂axioms␈α⊂␈↓↓n1 < n2,␈α∂n2 < n3,

␈↓ α∧␈↓↓n3 < n4␈↓,␈α∂etc.␈α∞and␈α∂the␈α∞general␈α∂axioms␈α∞␈↓↓∀x y.x < y ⊃ x ≠ y␈↓␈α∂and␈α∂␈↓↓∀x y z. x < y ∧ y < z ⊃ x < z␈↓.␈α∞ This

␈↓ α∧␈↓makes␈αthe␈αnumber␈α
of␈αaxioms␈αproportional␈α
to␈αthe␈αnumber␈αof␈α
names.␈α A␈αthird␈α
possibility␈αinvolves

␈↓ α∧␈↓mapping␈α∞the␈α
names␈α∞onto␈α∞integers␈α
with␈α∞axioms␈α
like␈α∞␈↓↓index n1 = 1,␈α∞index n2 = 2␈↓,␈α
etc.␈α∞and␈α∞using␈α
a


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f12


␈↓ α∧␈↓theory␈α
of␈α
the␈α
integers␈α
that␈α
provides␈α∞for␈α
their␈α
distinctness.␈α
 The␈α
fourth␈α
possibility␈α∞involves␈α
using

␈↓ α∧␈↓string␈α⊃constants␈α⊂for␈α⊃the␈α⊃names␈α⊂and␈α⊃"attaching"␈α⊃to␈α⊂equality␈α⊃in␈α⊃the␈α⊂language␈α⊃a␈α⊃subroutine␈α⊂that

␈↓ α∧␈↓computes␈α⊂whether␈α⊂two␈α⊂strings␈α⊂are␈α∂equal.␈α⊂ If␈α⊂our␈α⊂names␈α⊂were␈α∂quoted␈α⊂symbols␈α⊂as␈α⊂in␈α⊂LISP,␈α∂this

␈↓ α∧␈↓amounts␈α∂to␈α∂having␈α∂␈↓↓'a ≠ 'b␈↓␈α∂and␈α∂all␈α∂its␈α∞countable␈α∂infinity␈α∂of␈α∂analogs␈α∂as␈α∂axioms.␈α∂ Each␈α∂of␈α∞these

␈↓ α∧␈↓devices is useful in appropriate circumstances.

␈↓ α∧␈↓␈↓ αTFrom␈α∞the␈α∞point␈α∞of␈α
view␈α∞of␈α∞mathematical␈α∞logic,␈α
there␈α∞is␈α∞no␈α∞harm␈α
in␈α∞having␈α∞an␈α∞infinity␈α
of

␈↓ α∧␈↓such␈α∞axioms.␈α∞ From␈α∞the␈α∂computational␈α∞point␈α∞of␈α∞view␈α∞of␈α∂a␈α∞theorem␈α∞proving␈α∞or␈α∂problem␈α∞solving

␈↓ α∧␈↓program,␈α
we␈α
merely␈α
suppose␈α
that␈αwe␈α
rely␈α
on␈α
the␈α
computer␈αto␈α
generate␈α
the␈α
assertion␈α
that␈αtwo␈α
names

␈↓ α∧␈↓are␈α
distinct␈α
whenever␈α
this␈α
is␈α
required,␈α
since␈α
a␈α
subroutine␈α
can␈α
easily␈α
tell␈α
whether␈α
two␈α
strings␈αare␈α
the

␈↓ α∧␈↓same.

␈↓ α∧␈↓␈↓ αTBesides␈α∩axiomatizing␈α∩the␈α∩distinctness␈α∩of␈α∩the␈α∩constants,␈α∩we␈α∩also␈α∩want␈α∩to␈α∩axiomatize␈α∩the

␈↓ α∧␈↓distinctness␈α⊂of␈α⊂terms.␈α⊂ This␈α∂may␈α⊂be␈α⊂accomplished␈α⊂by␈α∂providing␈α⊂for␈α⊂each␈α⊂function␈α⊂two␈α∂axioms.

␈↓ α∧␈↓Letting ␈↓↓foo␈↓ be a function of two arguments we postulate

␈↓ α∧␈↓17)␈↓ αt ␈↓↓∀x1 x2 y1 y2.foo(x1,y1) = foo(x2,y2) ⊃ x1 = x2 ∧ y1 =y2␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓18)␈↓ αt ␈↓↓∀x y.fname foo(x,y) = 'foo␈↓.

␈↓ α∧␈↓The␈αfirst␈α
axiom␈αensures␈α
that␈αunless␈α
the␈αarguments␈αof␈α
␈↓↓foo␈↓␈αare␈α
identical,␈αits␈α
values␈αare␈αdistinct.␈α
 The

␈↓ α∧␈↓second␈α∞ensures␈α
that␈α∞the␈α∞values␈α
of␈α∞␈↓↓foo␈↓␈α∞are␈α
distinct␈α∞from␈α∞the␈α
values␈α∞of␈α∞any␈α
other␈α∞function␈α∞or␈α
any

␈↓ α∧␈↓constant, assuming that we refrain from naming any constant ␈↓↓'foo.␈↓

␈↓ α∧␈↓␈↓ αTThese␈α
axioms␈αamount␈α
to␈α
making␈αour␈α
domain␈αisomorphic␈α
to␈α
the␈αHerbrand␈α
universe␈α
of␈αthe

␈↓ α∧␈↓language.

␈↓ α∧␈↓␈↓ αTNow␈α⊃that␈α⊃the␈α⊃names␈α⊃are␈α⊃guaranteed␈α⊃distinct,␈α⊃what␈α⊃about␈α⊃the␈α⊃objects␈α⊃they␈α⊃denote?␈α⊂ We

␈↓ α∧␈↓introduce␈α∪a␈α∀predicate␈α∪␈↓↓e(x,y)␈↓␈α∪and␈α∀axiomatize␈α∪it␈α∀to␈α∪be␈α∪an␈α∀equivalence␈α∪relation.␈α∀ Its␈α∪intended

␈↓ α∧␈↓interpretation␈αis␈αthat␈αthe␈αnames␈α␈↓↓x␈↓␈αand␈α␈↓↓y␈↓␈αdenote␈αthe␈αsame␈αobject.␈α We␈αthen␈αformulate␈αall␈αour␈αusual


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f13


␈↓ α∧␈↓axioms␈αin␈αterms␈αof␈αnames␈αrather␈αthan␈αin␈αterms␈αof␈αobjects.␈α Thus␈α␈↓↓on(n1,n2)␈↓␈αmeans␈αthat␈αthe␈αobject

␈↓ α∧␈↓named␈α
by␈α
␈↓↓n1␈↓␈α
is␈α
on␈α
the␈α
object␈α
named␈α
by␈α
␈↓↓n2,␈↓␈α
and␈α
␈↓↓bird x␈↓␈α
means␈α
that␈α
the␈α
name␈α
␈↓↓x␈↓␈α
denotes␈α
a␈α
bird.

␈↓ α∧␈↓We␈α⊂add␈α⊂axioms␈α∂of␈α⊂substitutivity␈α⊂for␈α⊂␈↓↓e␈↓␈α∂with␈α⊂regard␈α⊂to␈α⊂those␈α∂predicates␈α⊂and␈α⊂functions␈α⊂that␈α∂are

␈↓ α∧␈↓translates␈αof␈αpredicates␈αreferring␈α
to␈αobjects␈αrather␈αthan␈α
predicates␈αon␈αthe␈αnames␈αthemselves.␈α
 Thus

␈↓ α∧␈↓we may have axioms

␈↓ α∧␈↓19)␈↓ αt ␈↓↓∀n1 n2 n1' n2'.e(n1,n1') ∧ e(n2,n2') ⊃ (on(n1,n2) ≡ on(n1',n2')␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓20)␈↓ αt␈↓↓∀x1 x2 y1 y2.e(x1,x2) ∧ e(y1,y2) ⊃ e(foo(x1,y1),foo(x2,y2))␈↓.

␈↓ α∧␈↓␈↓ αTIf␈αfor␈αsome␈αclass␈α␈↓↓C␈↓␈αof␈αnames,␈αwe␈αwish␈αto␈αassert␈αthe␈αunique␈αnames␈αhypothesis,␈αwe␈αsimply␈αuse

␈↓ α∧␈↓an axiom like

␈↓ α∧␈↓21)␈↓ αt ␈↓↓∀n1 n2.n1 ε C ∧ n2 ε C ⊃ (e(n1,n2) ≡ n1 = n2)␈↓.

␈↓ α∧␈↓␈↓ αTHowever,␈α
we␈α
often␈α
want␈αonly␈α
to␈α
assume␈α
that␈α
distinct␈αnames␈α
denote␈α
distinct␈α
objects␈αwhen␈α
this

␈↓ α∧␈↓doesn't␈αcontradict␈α
our␈αother␈αassumptions.␈α
 In␈αgeneral,␈α
our␈αaxioms␈αwon't␈α
permit␈αmaking␈α
all␈αnames

␈↓ α∧␈↓distinct␈α∂simultaneously,␈α⊂and␈α∂there␈α∂will␈α⊂be␈α∂several␈α∂models␈α⊂with␈α∂maximally␈α∂distinct␈α⊂objects.␈α∂ The

␈↓ α∧␈↓simplest example is obtained by circumscribing ␈↓↓e(x,y)␈↓ while adhering to the axiom

␈↓ α∧␈↓22)␈↓ αt ␈↓↓e(n1,n2) ∨ e(n1,n3)␈↓

␈↓ α∧␈↓where␈α∪␈↓↓n1,␈↓␈α∩␈↓↓n2,␈↓␈α∪and␈α∩␈↓↓n3␈↓␈α∪are␈α∩distinct␈α∪names.␈α∩ There␈α∪will␈α∩then␈α∪be␈α∩two␈α∪models,␈α∪one␈α∩satisfying

␈↓ α∧␈↓␈↓↓e(n1,n2) ∧ ¬e(n1,n3)␈↓ and the other satisfying ␈↓↓¬e(n1,n2) ∧ e(n1,n3).␈↓

␈↓ α∧␈↓␈↓ αTThus␈αcircumscribing␈α
␈↓↓e(x,y)␈↓␈αmaximizes␈α
uniqueness␈αof␈αnames.␈α
 If␈αwe␈α
only␈αwant␈αunique␈α
names

␈↓ α∧␈↓for␈αsome␈αclass␈α␈↓↓C␈↓␈αof␈αnames,␈αthen␈αwe␈αcircumscribe␈αthe␈αformula␈α␈↓↓x ε C ∧ y ε C ⊃ e(x,y)␈↓.␈α
 An␈αexample

␈↓ α∧␈↓of␈αsuch␈αa␈α
circumscription␈αis␈αgiven␈α
in␈αAppendix␈αB.␈α However,␈α
there␈αseems␈αto␈α
be␈αa␈αprice.␈α
 Part␈αof

␈↓ α∧␈↓the␈α
price␈αis␈α
admitting␈αnames␈α
as␈αobjects.␈α
 Another␈αpart␈α
is␈αadmitting␈α
the␈αpredicate␈α
␈↓↓e(x,y)␈↓␈α
which␈αis

␈↓ α∧␈↓substitutive␈αfor␈α
predicates␈αand␈αfunctions␈α
of␈αnames␈α
that␈αreally␈αare␈α
about␈αthe␈α
objects␈αdenoted␈αby␈α
the

␈↓ α∧␈↓names.␈α∂ ␈↓↓e(x,y)␈↓␈α∂is␈α∂not␈α∞to␈α∂be␈α∂taken␈α∂as␈α∞substitutive␈α∂for␈α∂predicates␈α∂on␈α∞names␈α∂that␈α∂aren't␈α∂about␈α∞the

␈↓ α∧␈↓objects.  Of these our only present example is equality.  Thus we don't have
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f14


␈↓ α∧␈↓* ␈↓↓∀n1 n2 n1' n2'.e(n1,n1') ∧ e(n2,n2') ⊃ (n1 = n2) ≡ n1' = n2')␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α
awkward␈αpart␈α
of␈αthe␈α
price␈αis␈α
that␈α
we␈αmust␈α
refrain␈αfrom␈α
any␈αfunctions␈α
whose␈αvalues␈α
are

␈↓ α∧␈↓the␈αobjects␈αthemselves␈αrather␈αthan␈αnames.␈α
 They␈αwould␈αspoil␈αthe␈αcircumscription␈αby␈α
not␈αallowing

␈↓ α∧␈↓us␈αto␈αinfer␈αthe␈αdistinctness␈αof␈αthe␈αobjects␈αdenoted␈αby␈αdistinct␈αnames.␈α Actually,␈αwe␈αcan␈αallow␈αthem

␈↓ α∧␈↓provided␈αwe␈αdon't␈αinclude␈αthe␈αaxioms␈αinvolving␈αthem␈αin␈αthe␈αcircumscription.␈α Unfortunately,␈αthis

␈↓ α∧␈↓spoils the other property of circumscription that lets us take any facts into account.

␈↓ α∧␈↓␈↓ αTThe␈α
examples␈α
of␈α
the␈α
use␈α
of␈α
circumscription␈α
in␈α
AI␈α
in␈α
the␈α
rest␈α
of␈α
the␈α
paper␈α
don't␈αinterpret␈α
the

␈↓ α∧␈↓variables␈α∞as␈α∞merely␈α∂ranging␈α∞over␈α∞names.␈α∞ Therefore,␈α∂they␈α∞are␈α∞incompatible␈α∞with␈α∂getting␈α∞unique

␈↓ α∧␈↓names␈αby␈αcircumscription␈αas␈αdescribed␈αin␈αthis␈αsection.␈α Presumably␈αit␈αwouldn't␈αbe␈αvery␈αdifficult␈αto

␈↓ α∧␈↓revise those axioms for compatibility with the present approach to unique names.


␈↓ α∧␈↓7. ␈↓αTwo examples of Raymond Reiter␈↓

␈↓ α∧␈↓␈↓ αTReiter␈α∃asks␈α∃about␈α∃representing,␈α∃"Quakers␈α∀are␈α∃normally␈α∃pacifists␈α∃and␈α∃Republicans␈α∀are

␈↓ α∧␈↓normally␈αnon-pacifists.␈α How␈αabout␈αNixon,␈αwho␈αis␈αboth␈αa␈αQuaker␈αand␈αa␈αRepublican?"␈αSystems␈αof

␈↓ α∧␈↓non-monotonic␈αreasoning␈α
that␈αuse␈α
non-provability␈αas␈α
a␈αbasis␈α
for␈αinferring␈α
negation␈αwill␈αinfer␈α
that

␈↓ α∧␈↓Nixon␈α∂is␈α∂neither␈α∂a␈α⊂pacifist␈α∂nor␈α∂a␈α∂non-pacifist.␈α⊂ Combining␈α∂these␈α∂conclusions␈α∂with␈α⊂the␈α∂original

␈↓ α∧␈↓premiss leads to a contradiction.

␈↓ α∧␈↓We use

␈↓ α∧␈↓23)␈↓ αt ␈↓↓∀x.quaker x ∧ ¬ab aspect1 x ⊃ pacifist x␈↓,

␈↓ α∧␈↓24)␈↓ αt ␈↓↓∀x.republican x ∧ ¬ab aspect2 x ⊃ ¬ pacifist x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓25)␈↓ αt ␈↓↓quaker Nixon ∧ republican Nixon␈↓.

␈↓ α∧␈↓␈↓ αTWhen␈α∞we␈α∞circumscribe␈α
␈↓↓ab z␈↓␈α∞using␈α∞these␈α
three␈α∞sentences␈α∞as␈α
␈↓↓A(ab,pacifist),␈↓␈α∞we␈α∞will␈α∞only␈α
be

␈↓ α∧␈↓able␈αto␈αconclude␈αthat␈αNixon␈αis␈αeither␈αabnormal␈αin␈α␈↓↓aspect1␈↓␈αor␈αin␈α␈↓↓aspect2,␈↓␈αand␈αwe␈αwill␈αnot␈αbe␈αable

␈↓ α∧␈↓to␈α⊂say␈α⊂whether␈α⊃he␈α⊂is␈α⊂a␈α⊃pacifist.␈α⊂ Of␈α⊂course,␈α⊂this␈α⊃is␈α⊂the␈α⊂same␈α⊃conclusion␈α⊂as␈α⊂would␈α⊃be␈α⊂reached

␈↓ α∧␈↓without circumscription.  The point is merely that we avoid contradiction.␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f15


␈↓ α∧␈↓␈↓ αTReiter's␈αsecond␈αexample␈αis␈αthat␈αa␈αperson␈αnormally␈αlives␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αwife␈α
and␈αin

␈↓ α∧␈↓the␈αsame␈αcity␈αas␈αhis␈αemployer.␈α But␈αA's␈αwife␈αlives␈αin␈αVancouver␈αand␈αA's␈αemployer␈αis␈αin␈αToronto.

␈↓ α∧␈↓We write

␈↓ α∧␈↓26)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ city x = city wife x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓27)␈↓ αt ␈↓↓∀x.¬ab aspect2 x ⊃ city x = city employer x␈↓.

␈↓ α∧␈↓If we have

␈↓ α∧␈↓28)␈↓ αt ␈↓↓city wife A = Vancouver ∧ city employer A = Toronto ∧ Toronto ≠ Vancouver␈↓,

␈↓ α∧␈↓we␈α∂will␈α∂again␈α∂only␈α∂be␈α∂able␈α∂to␈α∂conclude␈α⊂that␈α∂A␈α∂lives␈α∂either␈α∂in␈α∂Toronto␈α∂or␈α∂Vancouver.␈α⊂ In␈α∂this

␈↓ α∧␈↓circumscription,␈α
the␈α
function␈α
␈↓↓city␈↓␈α
must␈α
be␈α
taken␈α
as␈α
variable.␈α
 This␈α
might␈α
be␈α
considered␈α
not␈α
entirely

␈↓ α∧␈↓satisfactory.␈α If␈αone␈αknows␈αthat␈αa␈αperson␈αeither␈αdoesn't␈αlive␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αwife␈αor␈αdoesn't

␈↓ α∧␈↓live␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αemployer,␈αthen␈α
there␈αis␈αan␈αincreased␈αprobability␈αthat␈αhe␈αdoesn't␈αlive␈α
in

␈↓ α∧␈↓the␈αsame␈αcity␈αas␈αeither.␈α A␈αsystem␈αthat␈αdid␈αreasoning␈αof␈αthis␈αkind␈αwould␈αseem␈αto␈αrequire␈αa␈αlarger

␈↓ α∧␈↓body␈αof␈α
facts␈αand␈αperhaps␈α
more␈αexplicitly␈α
metamathematical␈αreasoning.␈α Not␈α
knowing␈αhow␈α
to␈αdo

␈↓ α∧␈↓that,␈α⊂we␈α⊃might␈α⊂want␈α⊃to␈α⊂use␈α⊃␈↓↓aspect1 x␈↓␈α⊂in␈α⊃both␈α⊂(26)␈α⊃and␈α⊂(27).␈α⊃ Then␈α⊂once␈α⊃we␈α⊂know␈α⊃we␈α⊂would

␈↓ α∧␈↓conclude nothing about his city once we knew that he wasn't in the same city as either.



␈↓ α∧␈↓8. ␈↓αA More general treatment of an ␈↓↓is-a␈↓α hierarchy␈↓

␈↓ α∧␈↓␈↓ αTThe␈α∞bird␈α∞example␈α∞works␈α∞fine␈α∞when␈α∞a␈α∞fixed␈α∞␈↓↓is-a␈↓␈α∞hierarchy␈α∞is␈α∞in␈α∞question.␈α∞ However,␈α
our

␈↓ α∧␈↓writing␈αthe␈αinheritance␈αcancellation␈αaxioms␈αdepended␈αon␈αknowing␈αexactly␈αfrom␈αwhat␈αhigher␈αlevel

␈↓ α∧␈↓the␈α∪properties␈α∩were␈α∪inherited.␈α∩ This␈α∪doesn't␈α∩correspond␈α∪to␈α∩my␈α∪intuition␈α∩of␈α∪how␈α∪we␈α∩humans

␈↓ α∧␈↓represent␈α∩inheritance.␈α∩ It␈α∩would␈α∪seem␈α∩rather␈α∩that␈α∩when␈α∩we␈α∪say␈α∩that␈α∩birds␈α∩can␈α∩fly,␈α∪we␈α∩don't

␈↓ α∧␈↓necessarily␈α∞have␈α∞in␈α∞mind␈α∞that␈α
an␈α∞inheritance␈α∞of␈α∞inability␈α∞to␈α
fly␈α∞from␈α∞things␈α∞in␈α∞general␈α∞is␈α
being

␈↓ α∧␈↓cancelled.␈α
 We␈α
can␈α
formulate␈α
inheritance␈α
of␈α
properties␈α
in␈α
a␈α
more␈α
general␈α
way␈α
provided␈α
we␈αreify

␈↓ α∧␈↓the properties.  Presumably there are many ways of doing this, but here's one that seems to work.
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f16


␈↓ α∧␈↓␈↓ αTThe␈α∂first␈α∂order␈α∂variables␈α∂of␈α∂our␈α∂theory␈α∂range␈α∂over␈α∂classes␈α∂of␈α∂objects␈α∂(denoted␈α∂by␈α∂␈↓↓c␈↓␈α∞with

␈↓ α∧␈↓numerical␈α
suffixes),␈αproperties␈α
(denoted␈αby␈α
␈↓↓p)␈↓␈α
and␈αobjects␈α
(denoted␈αby␈α
␈↓↓x).␈↓␈αWe␈α
don't␈α
identify␈αour

␈↓ α∧␈↓classes␈α⊗with␈α∃sets␈α⊗(or␈α⊗with␈α∃the␈α⊗classes␈α∃of␈α⊗GB␈α⊗set␈α∃theory).␈α⊗ In␈α∃particular,␈α⊗we␈α⊗don't␈α∃assume

␈↓ α∧␈↓extensionality.  We have several predicates:

␈↓ α∧␈↓␈↓ αT␈↓↓ordinarily(c,p)␈↓␈αmeans␈αthat␈αobjects␈αof␈αclass␈α␈↓↓c␈↓␈αordinarily␈αhave␈αproperty␈α␈↓↓p.␈↓␈α␈↓↓c1 ≤ c2␈↓␈αmeans␈αthat

␈↓ α∧␈↓class␈α␈↓↓c1␈↓␈α
ordinarily␈αinherits␈α
from␈αclass␈α
␈↓↓c2.␈↓␈αWe␈α
assume␈αthat␈α
this␈αrelation␈α
is␈αtransitive.␈α ␈↓↓in(x,c)␈↓␈α
means

␈↓ α∧␈↓that the object ␈↓↓x␈↓ is in class ␈↓↓c.␈↓ ␈↓↓ap(p,x)␈↓ means that property ␈↓↓p␈↓ applies to object ␈↓↓x.␈↓ Our axioms are

␈↓ α∧␈↓29)␈↓ αt ␈↓↓∀c1 c2 c3. c1 ≤ c2 ∧ c2 ≤ c3 ⊃ c1 ≤ c3␈↓,

␈↓ α∧␈↓30)␈↓ αt ␈↓↓∀c1 c2 p.ordinarily(c2,p) ∧ c1 ≤ c2 ∧ ¬ab aspect1(c1,c2,p) ⊃ ordinarily(c1,p)␈↓,

␈↓ α∧␈↓31)␈↓ αt ␈↓↓∀c1 c2 c3 p.c1 ≤ c2 ∧ c2 ≤ c3 ∧ ordinarily(c2, not p) ⊃ ab aspect1(c1,c3,p)␈↓,

␈↓ α∧␈↓32)␈↓ αt ␈↓↓∀x c p.in(x,c) ∧ ordinarily(c,p) ∧ ¬ab aspect3(x,c,p) ⊃ ap(p,x)␈↓,

␈↓ α∧␈↓33)␈↓ αt ␈↓↓∀x c1 c2 p.in(x,c1) ∧ c1 ≤ c2 ∧ ordinarily(c1,not p) ⊃ ab aspect3(x,c2,p)␈↓.

␈↓ α∧␈↓(29)␈α
is␈α
the␈α
afore-mentioned␈α
transitivity␈αof␈α
≤.␈α
 (30)␈α
says␈α
that␈αproperties␈α
that␈α
ordinarily␈α
hold␈α
for␈αa

␈↓ α∧␈↓class␈α⊃are␈α⊃inherited␈α∩unless␈α⊃something␈α⊃is␈α∩abnormal.␈α⊃ (31)␈α⊃cancels␈α⊃the␈α∩inheritance␈α⊃if␈α⊃there␈α∩is␈α⊃an

␈↓ α∧␈↓intermediate␈αclass␈αfor␈αwhich␈αthe␈αproperty␈αordinarily␈αdoesn't␈αhold.␈α (32)␈αsays␈αthat␈αproperties␈αwhich

␈↓ α∧␈↓ordinarily␈αhold␈αactually␈αhold␈αfor␈αelements␈αof␈αthe␈αclass␈αunless␈αsomething␈αis␈αabnormal.␈α (33)␈αcancels

␈↓ α∧␈↓the␈α⊂effect␈α⊂of␈α⊂(32)␈α⊂when␈α∂there␈α⊂is␈α⊂an␈α⊂intermediate␈α⊂class␈α∂for␈α⊂which␈α⊂the␈α⊂negation␈α⊂of␈α⊂the␈α∂property

␈↓ α∧␈↓ordinarily␈α⊂holds.␈α⊃ Notice␈α⊂that␈α⊃this␈α⊂reification␈α⊂of␈α⊃properties␈α⊂seems␈α⊃to␈α⊂require␈α⊃imitation␈α⊂boolean

␈↓ α∧␈↓operators.  Such operators are discussed in (McCarthy 1979).



␈↓ α∧␈↓9. ␈↓αThe blocks world␈↓

␈↓ α∧␈↓␈↓ αTThe␈α
following␈α
set␈α
of␈α"situation␈α
calculus"␈α
axioms␈α
solves␈α
the␈αframe␈α
problem␈α
for␈α
a␈αblocks␈α
world

␈↓ α∧␈↓in␈α∂which␈α∞blocks␈α∂can␈α∞be␈α∂moved␈α∞and␈α∂painted.␈α∞ Here␈α∂␈↓↓result(e,s)␈↓␈α∞denotes␈α∂the␈α∞situation␈α∂that␈α∞results

␈↓ α∧␈↓when␈α
event␈α␈↓↓e␈↓␈α
occurs␈αin␈α
situation␈α␈↓↓s.␈↓␈α
The␈αformalism␈α
is␈αapproximately␈α
that␈αof␈α
(McCarthy␈αand␈α
Hayes

␈↓ α∧␈↓1969).
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f17


␈↓ α∧␈↓34)␈↓ αt ␈↓↓∀x e s.¬ab aspect1(x,e,s) ⊃ location(x,result(e,s)) = location(x,s)␈↓.

␈↓ α∧␈↓35)␈↓ αt ␈↓↓∀x e s.¬ab aspect2(x,e,s) ⊃ color(x,result(e,s)) = color(x,s)␈↓.

␈↓ α∧␈↓Objects change their locations and colors only for a reason.

␈↓ α∧␈↓36)␈↓ αt ␈↓↓∀x l s.ab aspect1(x,move(x,l),s)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓∀x l s.¬ab aspect3(x,l,s) ⊃ location(x,result(move(x,l),s)) = l␈↓.

␈↓ α∧␈↓37)␈↓ αt ␈↓↓∀x c s.ab aspect2(x,paint(x,c),s)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓∀x c s.¬ab aspect4(x,c,s) ⊃ color(x,result(paint(x,c),s)) = c␈↓.

␈↓ α∧␈↓Objects change their locations when moved and their colors when painted.

␈↓ α∧␈↓38)␈↓ αt ␈↓↓∀x l s.¬clear(top x,s) ∨ ¬clear(l,s) ∨ tooheavy x ∨ l = top x ⊃ ab aspect3(x,move(x,l),s)␈↓.

␈↓ α∧␈↓This␈αprevents␈αthe␈αrule␈α(36)␈αfrom␈αbeing␈αused␈αto␈αinfer␈αthat␈αan␈αobject␈αwill␈αmove␈αif␈αit␈αisn't␈αclear␈αor␈α
to

␈↓ α∧␈↓a␈αdestination␈αthat␈αisn't␈αclear␈αor␈αif␈αthe␈αobject␈αis␈αtoo␈αheavy.␈α An␈αobject␈αalso␈αcannot␈αbe␈αmoved␈αto␈αits

␈↓ α∧␈↓own top.

␈↓ α∧␈↓39)␈↓ αt ␈↓↓∀l s.clear(l,s) ≡ ¬∃x.(¬trivial x ∧ location(x,s) = l)␈↓.

␈↓ α∧␈↓A location is clear if all the objects there are trivial, e.g. a speck of dust.

␈↓ α∧␈↓40)␈↓ αt ␈↓↓∀x.¬ab aspect7 x ⊃ ¬trivial x␈↓.

␈↓ α∧␈↓Trivial objects are abnormal in ␈↓↓aspect7␈↓.



␈↓ α∧␈↓10. ␈↓αAn example of doing the circumscription.␈↓

␈↓ α∧␈↓␈↓ αTIn␈αorder␈αto␈αkeep␈αthe␈α
example␈αshort␈αwe␈αwill␈αtake␈α
into␈αaccount␈αonly␈αthe␈αfollowing␈α
facts␈αfrom

␈↓ α∧␈↓the earlier section on flying.

␈↓ α∧␈↓2) ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓3) ␈↓↓∀x.bird x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓4) ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f18


␈↓ α∧␈↓5) ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓7) ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓␈↓ αTTheir␈α
conjunction␈α
is␈α
taken␈α
as␈α
␈↓↓A(ab,flies)␈↓.␈α This␈α
means␈α
that␈α
what␈α
entities␈α
satisfy␈α
␈↓↓ab␈↓␈αand␈α
what

␈↓ α∧␈↓entities␈α⊃satisfy␈α⊃␈↓↓flies␈↓␈α⊃are␈α⊃to␈α⊃be␈α⊃verified␈α⊃so␈α⊃as␈α⊃to␈α⊃minimize␈α⊃␈↓↓ab z.␈↓␈α⊃Which␈α⊃objects␈α⊃are␈α∩birds␈α⊃and

␈↓ α∧␈↓ostriches are parameters rather than variables, i.e.  what objects are birds is considered given.

␈↓ α∧␈↓␈↓ αTWe␈α
also␈αneed␈α
an␈αaxiom␈α
that␈α
asserts␈αthat␈α
the␈αaspects␈α
are␈α
different.␈α Here␈α
is␈αa␈α
straightforward

␈↓ α∧␈↓version that would be rather long were there more than three aspects.

␈↓ α∧␈↓␈↓↓(∀x y.¬(aspect1 x = aspect2 y))

␈↓ α∧␈↓↓∧ (∀x y.¬(aspect1 x = aspect3 y))

␈↓ α∧␈↓↓∧ (∀x y.¬(aspect2 x = aspect3 y))

␈↓ α∧␈↓↓∧ (∀x y.aspect1 x = aspect1 y ≡ x =y)

␈↓ α∧␈↓↓∧ (∀x y.aspect2 x = aspect2 y ≡ x =y)

␈↓ α∧␈↓↓∧ (∀x y.aspect3 x = aspect3 y ≡ x =y).␈↓

␈↓ α∧␈↓The circumscription formula ␈↓↓A'(ab,flies)␈↓ is then

␈↓ α∧␈↓41)␈↓ αt ␈↓↓A(ab,flies) ∧ ∀ab' flies'.[A(ab',flies') ∧ [∀x. ab' x ⊃ ab x] ⊃ [∀x. ab x ≡ ab' x]]␈↓,

␈↓ α∧␈↓which spelled out becomes

␈↓ α∧␈↓42)␈↓ αt␈α␈↓↓[∀x.¬ab␈α
aspect1␈αx␈α
⊃␈α¬flies␈αx]␈α
∧␈α[∀x.bird␈α
x␈α⊃␈α
ab␈αaspect1␈αx]␈α
∧␈α[∀x.bird␈α
x␈α∧␈α
¬ab␈αaspect2␈αx␈α
⊃

␈↓ α∧␈↓↓flies␈α⊃x]␈α⊃∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃⊃␈α⊃ab␈α⊃aspect2␈α⊃x]␈α∩∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃∧␈α⊃¬ab␈α⊃aspect3␈α⊃x␈α⊃⊃␈α⊃¬flies␈α⊃x]␈α∩∧␈α⊃∀ab'

␈↓ α∧␈↓↓flies'.[[∀x.¬ab'␈αaspect1␈αx␈α⊃␈α¬flies'␈αx]␈α∧␈α[∀x.bird␈αx␈α⊃␈αab'␈αaspect1␈αx]␈α∧␈α[∀x.bird␈αx␈α∧␈α¬ab'␈αaspect2␈αx

␈↓ α∧␈↓↓⊃␈α
flies'␈α
x]␈α
∧␈α
[∀x.ostrich␈αx␈α
⊃␈α
ab'␈α
aspect2␈α
x]␈α∧␈α
[∀x.ostrich␈α
x␈α
∧␈α
¬ab'␈α
aspect3␈αx␈α
⊃␈α
¬flies'␈α
x]␈α
∧␈α[∀z.ab'␈α
z

␈↓ α∧␈↓↓⊃ ab z] ⊃ [∀z.ab z ≡ ab' z]]␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓A(ab,flies)␈↓␈α
is␈α
guaranteed␈α
to␈α
be␈α
true,␈α
because␈α
it␈α
is␈α
part␈α
of␈α
what␈α
is␈α
assumed␈α
in␈α
our␈αcommon

␈↓ α∧␈↓sense data base.  Therefore (42) reduces to

␈↓ α∧␈↓43)␈↓ αt␈↓↓∀ab'␈αflies'.[[∀x.¬ab'␈αaspect1␈α
x␈α⊃␈α¬flies'␈α
x]␈α∧␈α[∀x.bird␈αx␈α
⊃␈αab'␈αaspect1␈α
x]␈α∧␈α[∀x.bird␈α
x␈α∧


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f19


␈↓ α∧␈↓↓¬ab'␈α∂aspect2␈α∞x␈α∂⊃␈α∞flies'␈α∂x]␈α∞∧␈α∂[∀x.ostrich␈α∞x␈α∂⊃␈α∞ab'␈α∂aspect2␈α∞x]␈α∂∧␈α∞[∀x.ostrich␈α∂x␈α∞∧␈α∂¬ab'␈α∞aspect3␈α∂x␈α∞⊃

␈↓ α∧␈↓↓¬flies' x] ∧ [∀z.ab' z ⊃ ab z] ⊃ [∀z.ab z ≡ ab' z]]␈↓.

␈↓ α∧␈↓␈↓ αTOur␈αobjective␈αis␈αnow␈αto␈αmake␈αsuitable␈αsubstitutions␈αfor␈α␈↓↓ab'␈↓␈αand␈α␈↓↓flies'␈↓␈αso␈αthat␈αall␈α
the␈αterms

␈↓ α∧␈↓preceding␈α∞the␈α∞⊃␈α∞(43)␈α∞will␈α∞be␈α∞true,␈α∂and␈α∞right␈α∞side␈α∞will␈α∞determine␈α∞␈↓↓ab.␈↓␈α∞The␈α∞axiom␈α∂␈↓↓A(ab,flies)␈↓␈α∞will

␈↓ α∧␈↓then␈α
determine␈α∞␈↓↓flies,␈↓␈α
i.e.␈α
we␈α∞will␈α
know␈α
what␈α∞the␈α
fliers␈α
are.␈α∞ ␈↓↓flies'␈↓␈α
is␈α
easy,␈α∞because␈α
we␈α∞need␈α
only

␈↓ α∧␈↓apply␈αwishful␈αthinking;␈αwe␈αwant␈αthe␈αfliers␈αto␈αbe␈αjust␈αthose␈αbirds␈αthat␈αaren't␈αostriches.␈α Therefore,

␈↓ α∧␈↓we put

␈↓ α∧␈↓44)␈↓ αt ␈↓↓flies' x ≡ bird x ∧ ¬ostrich x␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓ab'␈↓ isn't really much more difficult, but there is a notational problem.  We define

␈↓ α∧␈↓45)␈↓ αt ␈↓↓ab' z ≡ [∃x.bird x ∧ z = aspect1 x] ∨ [∃x.ostrich x ∧ z = aspect2 x]␈↓,

␈↓ α∧␈↓which covers the cases we want to be abnormal.

␈↓ α∧␈↓␈↓ αTAppendix␈α∂A␈α∂contains␈α∂a␈α∞complete␈α∂proof␈α∂as␈α∂accepted␈α∞by␈α∂Jussi␈α∂Ketonen's␈α∂(1984)␈α∞interactive

␈↓ α∧␈↓theorem␈α⊂prover␈α⊂EKL.␈α⊂ EKL␈α⊂uses␈α∂the␈α⊂theory␈α⊂of␈α⊂types␈α⊂and␈α∂therefore␈α⊂has␈α⊂no␈α⊂problem␈α⊂with␈α∂the

␈↓ α∧␈↓second order logic required by circumscription.



␈↓ α∧␈↓11. ␈↓αPrioritized circumscription␈↓

␈↓ α∧␈↓␈↓ αTAn␈α∂alternate␈α∂way␈α∂of␈α∂introducing␈α∂formula␈α∞circumscription␈α∂is␈α∂by␈α∂means␈α∂of␈α∂an␈α∂ordering␈α∞on

␈↓ α∧␈↓tuples of predicates satisfying an axiom.  We define ␈↓↓P ≤ P'␈↓ by

␈↓ α∧␈↓46)␈↓ αt ␈↓↓∀P P'.P ≤ P' ≡ ∀x.E(P,x) ⊃ E(P',x)␈↓.

␈↓ α∧␈↓That ␈↓↓P0␈↓ is a relative minimum in this ordering is expressed by

␈↓ α∧␈↓47)␈↓ αt ␈↓↓∀P.P ≤ P0 ⊃ P = P0␈↓,

␈↓ α∧␈↓where equality is interpreted extensionally, i.e. we have

␈↓ α∧␈↓48)␈↓ αt ␈↓↓∀P P'.P = P' ≡ (∀x.E(P,x) ≡ E(P',x))␈↓.

␈↓ α∧␈↓Assuming␈αthat␈αwe␈αlook␈αfor␈αa␈αminimum␈αamong␈αpredicates␈α␈↓↓P␈↓␈αsatisfying␈α␈↓↓A(P),␈↓␈αthen␈α(46)␈αexpands␈αto


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f20


␈↓ α∧␈↓precisely␈α∞to␈α∂the␈α∞circumscription␈α∂formula␈α∞(1).␈α∞ In␈α∂some␈α∞earlier␈α∂expositions␈α∞of␈α∂circumscription␈α∞this

␈↓ α∧␈↓ordering␈αapproach␈α
was␈αused,␈α
and␈αVladimir␈α
Lifschitz␈αin␈α
a␈αrecent␈α
seminar␈αadvocated␈α
returning␈αto␈α
it

␈↓ α∧␈↓as a more fundamental and understandable concept.

␈↓ α∧␈↓␈↓ αTI'm␈αbeginning␈αto␈αthink␈αhe's␈α
right␈αabout␈αit␈αbeing␈αmore␈α
understandable,␈αbut␈αthere␈αseems␈αto␈α
be

␈↓ α∧␈↓a␈α
more␈αfundamental␈α
reason␈αfor␈α
using␈αit.␈α
 Namely,␈αcertain␈α
common␈αsense␈α
axiomatizations␈αare␈α
easier

␈↓ α∧␈↓to␈αformalize␈α
if␈αwe␈αuse␈α
a␈αnew␈αkind␈α
of␈αordering,␈αand␈α
circumscription␈αbased␈αon␈α
this␈αkind␈αof␈α
ordering

␈↓ α∧␈↓doesn't seem to reduce to ordinary formula circumscription.

␈↓ α∧␈↓␈↓ αTWe call it ␈↓αprioritized circumscription␈↓.

␈↓ α∧␈↓␈↓ αTSuppose we write some bird axioms in the form

␈↓ α∧␈↓49)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓50)␈↓ αt ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α
intent␈αis␈α
clear.␈α
 The␈αgoal␈α
is␈α
that␈αbeing␈α
a␈α
bird␈αand␈α
not␈α
abnormal␈αin␈α
␈↓↓aspect2␈↓␈αprevents␈α
the

␈↓ α∧␈↓application␈α
of␈α(49).␈α
 However,␈α
circumscribing␈α␈↓↓ab z␈↓␈α
with␈α
the␈αconjunction␈α
of␈α
(49)␈αand␈α
(50)␈α
as␈α␈↓↓A(ab)␈↓

␈↓ α∧␈↓doesn't have this effect, because (50) is equivalent to

␈↓ α∧␈↓51)␈↓ αt ␈↓↓∀x.bird x ⊃ ab aspect1 x ∨ ab aspect2 x␈↓,

␈↓ α∧␈↓and␈α⊃there␈α⊃is␈α∩no␈α⊃indication␈α⊃that␈α⊃one␈α∩would␈α⊃prefer␈α⊃to␈α⊃have␈α∩␈↓↓aspect1 x␈↓␈α⊃abnormal␈α⊃than␈α∩to␈α⊃have

␈↓ α∧␈↓␈↓↓aspect2 x␈↓␈α∂abnormal.␈α∞ Circumscription␈α∂then␈α∞results␈α∂in␈α∞a␈α∂disjunction␈α∞which␈α∂is␈α∞not␈α∂wanted␈α∂in␈α∞this

␈↓ α∧␈↓case.  The need to avoid this disjunction is why the axioms were written as they are in section 4.

␈↓ α∧␈↓␈↓ αTHowever,␈αby␈αusing␈αa␈α
new␈αkind␈αof␈αordering␈αwe␈α
can␈αleave␈α(49)␈αand␈α(50)␈α
as␈αis,␈αand␈αstill␈αget␈α
the

␈↓ α∧␈↓desired effect.

␈↓ α∧␈↓␈↓ αTWe define two orderings on ␈↓↓ab␈↓ predicates, namely

␈↓ α∧␈↓52)␈↓ αt ␈↓↓∀ab ab'.ab ≤␈↓β1␈↓↓ ab' ≡ ∀x.ab aspect1 x ⊃ ab' aspect1 x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓53)␈↓ αt ␈↓↓∀ab ab'.ab ≤␈↓β2␈↓↓ ab' ≡ ∀x.ab aspect2 x ⊃ ab' aspect2 x␈↓.
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f21


␈↓ α∧␈↓We then combine these orderings lexicographically giving ␈↓↓≤␈↓β2␈↓↓␈↓ priority over ␈↓↓≤␈↓β1␈↓↓␈↓ getting

␈↓ α∧␈↓54)␈↓ αt ␈↓↓∀ab ab'.ab ≤␈↓β1<2␈↓↓ ab' ≡ ab ≤␈↓β2␈↓↓ ab' ∨ ab =␈↓β2␈↓↓ ab' ∧ ab ≤␈↓β1␈↓↓ ab'␈↓.

␈↓ α∧␈↓␈↓ αTChoosing␈α∞␈↓↓ab0␈↓␈α∂so␈α∞as␈α∞to␈α∂minimize␈α∞this␈α∞ordering␈α∂yields␈α∞the␈α∞result␈α∂that␈α∞exactly␈α∞birds␈α∂can␈α∞fly.

␈↓ α∧␈↓However, if we add

␈↓ α∧␈↓55)␈↓ αt ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓,

␈↓ α∧␈↓we'll␈αget␈α
that␈αostriches␈α(whether␈α
or␈αnot␈αostriches␈α
are␈αbirds)␈α
don't␈αfly␈αwithout␈α
further␈αaxioms.␈α If␈α
we

␈↓ α∧␈↓use

␈↓ α∧␈↓56)␈↓ αt ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ab aspect2 x␈↓

␈↓ α∧␈↓instead␈α⊂of␈α⊂(55),␈α⊂we'll␈α⊂have␈α∂to␈α⊂revise␈α⊂our␈α⊂notion␈α⊂of␈α∂ordering␈α⊂to␈α⊂put␈α⊂minimizing␈α⊂␈↓↓ab aspect3 x␈↓␈α∂at

␈↓ α∧␈↓higher␈α∩priority␈α∩than␈α⊃minimizing␈α∩␈↓↓aspect2 x␈↓␈α∩and␈α⊃␈↓↓a␈α∩fortiori␈↓␈α∩at␈α⊃higher␈α∩priority␈α∩than␈α⊃minimizing

␈↓ α∧␈↓␈↓↓aspect1.␈↓

␈↓ α∧␈↓␈↓ αTThis␈αsuggests␈αproviding␈αa␈αpartial␈αordering␈αon␈αaspects␈αgiving␈αtheir␈αpriorities␈αand␈αproviding

␈↓ α∧␈↓axioms␈α∂that␈α∞permit␈α∂deducing␈α∂the␈α∞ordering␈α∂on␈α∂␈↓↓ab␈↓␈α∞from␈α∂the␈α∂sentences␈α∞that␈α∂describe␈α∂the␈α∞ordering

␈↓ α∧␈↓relations.␈α⊂ We␈α⊂haven't␈α∂been␈α⊂able␈α⊂to␈α⊂work␈α∂this␈α⊂out␈α⊂yet.␈α⊂ It␈α∂would␈α⊂apparently␈α⊂be␈α⊂a␈α∂considerable

␈↓ α∧␈↓elaboration of the formalism.

␈↓ α∧␈↓␈↓ αTI␈α⊃am␈α⊃hopeful␈α⊃that␈α⊃␈↓↓prioritized␈α⊃circumscription␈↓␈α⊃will␈α⊃turn␈α⊃out␈α⊃to␈α⊃be␈α⊃the␈α⊃most␈α∩natural␈α⊃and

␈↓ α∧␈↓powerful variant.



␈↓ α∧␈↓12. ␈↓αGeneral considerations and remarks␈↓

␈↓ α∧␈↓␈↓ αT1.␈α
Suppose␈α
we␈α
have␈α
a␈α
data␈α
base␈αof␈α
facts␈α
axiomatized␈α
by␈α
a␈α
formalism␈α
involving␈αthe␈α
predicate

␈↓ α∧␈↓␈↓↓ab.␈↓␈α∩In␈α∩connection␈α∩with␈α∩a␈α∩particular␈α∩problem,␈α∩a␈α∩program␈α∩takes␈α∩a␈α∩subcollection␈α∩of␈α∩these␈α⊃facts

␈↓ α∧␈↓together␈α
with␈α
the␈αspecific␈α
facts␈α
of␈αthe␈α
problem␈α
and␈αthen␈α
circumscribes␈α
␈↓↓ab z.␈↓␈αWe␈α
get␈α
a␈αsecond␈α
order

␈↓ α∧␈↓formula,␈αand␈αin␈αgeneral,␈αas␈αthe␈αnatural␈αnumber␈αexample␈αof␈α(McCarthy␈α1980)␈αshows,␈αthis␈αformula

␈↓ α∧␈↓is␈α∀not␈α∀equivalent␈α∀to␈α∃any␈α∀first␈α∀order␈α∀formula.␈α∃ However,␈α∀many␈α∀common␈α∀sense␈α∃domains␈α∀are


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f22


␈↓ α∧␈↓axiomatizable␈α∞in␈α
such␈α∞a␈α
way␈α∞that␈α
the␈α∞circumscription␈α
is␈α∞equivalent␈α
to␈α∞a␈α
first␈α∞order␈α∞formula.␈α
 In

␈↓ α∧␈↓this␈α∂case␈α∞we␈α∂call␈α∞the␈α∂circumscription␈α∞collapsible.␈α∂ For␈α∞example,␈α∂Vladimir␈α∂Lifschitz␈α∞(unpublished

␈↓ α∧␈↓1983␈α∞and␈α∞1984)␈α∞has␈α∞shown␈α∞that␈α∞this␈α∞is␈α∞true␈α
if␈α∞the␈α∞axioms␈α∞are␈α∞from␈α∞a␈α∞certain␈α∞class␈α∞of␈α
universal

␈↓ α∧␈↓formulas␈α
and␈α
there␈αare␈α
no␈α
functions.␈α
 This␈αcan␈α
presumably␈α
be␈α
extended␈αto␈α
other␈α
cases␈α
in␈αwhich

␈↓ α∧␈↓the␈α∞ranges␈α∞and␈α∞domains␈α∞of␈α
the␈α∞functions␈α∞are␈α∞disjoint,␈α∞so␈α∞that␈α
there␈α∞is␈α∞no␈α∞way␈α∞of␈α∞generating␈α
an

␈↓ α∧␈↓infinity of elements.

␈↓ α∧␈↓␈↓ αTCircumscription␈α∞is␈α∂also␈α∞collapsible␈α∂when␈α∞the␈α∂predicates␈α∞are␈α∂all␈α∞monadic␈α∂and␈α∞there␈α∂are␈α∞no

␈↓ α∧␈↓functions.

␈↓ α∧␈↓␈↓ αTWe␈α⊃can␈α⊃then␈α⊃regard␈α⊃the␈α⊃process␈α⊃of␈α⊃deciding␈α⊃what␈α⊃facts␈α⊃to␈α⊃take␈α⊃into␈α⊃account␈α⊃and␈α⊂then

␈↓ α∧␈↓circumscribing␈α
as␈α
a␈αprocess␈α
of␈α
compiling␈αfrom␈α
a␈α
slightly␈αhigher␈α
level␈α
non-monotonic␈αlanguage␈α
into

␈↓ α∧␈↓mathematical␈α∞logic,␈α∂especially␈α∞first␈α∂order␈α∞logic.␈α∂ We␈α∞can␈α∂also␈α∞regard␈α∂natural␈α∞language␈α∂as␈α∞higher

␈↓ α∧␈↓level␈α∀than␈α∀logic.␈α∀ However,␈α∀as␈α∀I␈α∀shall␈α∀discuss␈α∀elsewhere,␈α∀natural␈α∀language␈α∀doesn't␈α∃have␈α∀an

␈↓ α∧␈↓independent␈α∪reasoning␈α∪process,␈α∪because␈α∪most␈α∪natural␈α∪language␈α∪inferences␈α∀involve␈α∪suppressed

␈↓ α∧␈↓premisses␈α∞which␈α∞are␈α∞not␈α∂represented␈α∞in␈α∞natural␈α∞language␈α∞in␈α∂the␈α∞minds␈α∞of␈α∞the␈α∞people␈α∂doing␈α∞the

␈↓ α∧␈↓reasoning.

␈↓ α∧␈↓␈↓ αTReiter␈αhas␈αpointed␈αout,␈αboth␈αinformally␈αand␈αimplicitly␈αin␈α(Reiter␈α1982)␈αthat␈αcircumscription

␈↓ α∧␈↓often␈α∂translates␈α⊂directly␈α∂into␈α⊂Prolog␈α∂program␈α∂once␈α⊂it␈α∂has␈α⊂been␈α∂decided␈α∂what␈α⊂facts␈α∂to␈α⊂take␈α∂into

␈↓ α∧␈↓account.

␈↓ α∧␈↓␈↓ αT2.␈α∂Circumscription␈α∂has␈α∞interesting␈α∂relations␈α∂to␈α∞Reiter's␈α∂(1980)␈α∂logic␈α∞of␈α∂defaults.␈α∂ In␈α∞simple

␈↓ α∧␈↓cases␈αthey␈αgive␈α
the␈αsame␈αresults.␈α However,␈α
a␈αcomputer␈αprogram␈αusing␈α
default␈αlogic␈αwould␈αhave␈α
to

␈↓ α∧␈↓establish␈α∞the␈α∞existence␈α∞of␈α∂models,␈α∞perhaps␈α∞by␈α∞constructing␈α∞them,␈α∂in␈α∞order␈α∞to␈α∞determine␈α∂that␈α∞the

␈↓ α∧␈↓sentences␈α∞mentioned␈α∞in␈α∞default␈α
rules␈α∞were␈α∞consistent.␈α∞ Such␈α
computations␈α∞are␈α∞not␈α∞just␈α
selectively

␈↓ α∧␈↓applying␈α⊂the␈α⊂rules␈α⊃of␈α⊂inference␈α⊂of␈α⊃logic␈α⊂but␈α⊂are␈α⊂metamathematical.␈α⊃ At␈α⊂present␈α⊂this␈α⊃is␈α⊂treated

␈↓ α∧␈↓entirely␈α∞informally,␈α∞and␈α∂I␈α∞am␈α∞not␈α∂aware␈α∞of␈α∞any␈α∂computer␈α∞program␈α∞that␈α∂finds␈α∞models␈α∞of␈α∂sets␈α∞of

␈↓ α∧␈↓sentences or even interacts with a user to find and verify such models.
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f23


␈↓ α∧␈↓␈↓ αTCircumscription␈αworks␈α
entirely␈αwithin␈α
the␈αlogic␈α
as␈αAppendices␈α
A␈αand␈α
B␈αillustrate.␈α
 It␈αcan␈α
do

␈↓ α∧␈↓this,␈αbecause␈αit␈αuses␈αsecond␈αorder␈αlogic␈αto␈αimport␈αsome␈αof␈αthe␈αmodel␈αtheory␈αof␈αfirst␈αorder␈αformulas

␈↓ α∧␈↓into␈αthe␈αtheory␈αitself.␈α Finding␈αthe␈αright␈αsubstitution␈αfor␈αthe␈αpredicate␈αvariables␈αis,␈αin␈αthe␈αcases␈αwe

␈↓ α∧␈↓have␈αexamined,␈αthe␈αsame␈αtask␈αas␈αfinding␈αmodels␈αof␈αa␈αfirst␈αorder␈αtheory.␈α Putting␈α
everything␈αinto

␈↓ α∧␈↓the␈α∂logic␈α⊂itself␈α∂is␈α∂an␈α⊂advantage␈α∂as␈α∂long␈α⊂as␈α∂there␈α∂is␈α⊂neither␈α∂a␈α∂good␈α⊂theory␈α∂of␈α∂how␈α⊂to␈α∂construct

␈↓ α∧␈↓models nor programs that do it.

␈↓ α∧␈↓␈↓ αTNotice,␈α∂however,␈α∂that␈α∂finding␈α∂an␈α∂interpretation␈α∂of␈α∂a␈α∂language␈α∂has␈α∂two␈α∂parts␈α∂-␈α∂finding␈α∂a

␈↓ α∧␈↓domain␈α∂and␈α∂interpreting␈α∂the␈α∂predicate␈α∂and␈α∂function␈α∂letters␈α∂by␈α∂predicates␈α∂and␈α∂functions␈α⊂on␈α∂the

␈↓ α∧␈↓domain.␈α It␈αseems␈αthat␈αthe␈αsecond␈αis␈αeasier␈αto␈αimport␈αinto␈αsecond␈αorder␈αlogic␈αthan␈αthe␈α
first.␈α This

␈↓ α∧␈↓may be why our treatment of unique names is awkward.

␈↓ α∧␈↓␈↓ αT3.␈α
The␈α∞axioms␈α
introduced␈α
in␈α∞this␈α
paper␈α
are␈α∞still␈α
not␈α
in␈α∞a␈α
suitable␈α
form␈α∞for␈α
inclusion␈α∞in␈α
a

␈↓ α∧␈↓common␈αsense␈αdatabase.␈α Some␈αof␈αthe␈αcircumscriptions␈αhave␈αunwanted␈αconclusions,␈αe.g.␈αthat␈αthere

␈↓ α∧␈↓are␈α∀no␈α∀ostriches␈α∪if␈α∀none␈α∀are␈α∀explicitly␈α∪mentioned.␈α∀ Perhaps␈α∀some␈α∀of␈α∪this␈α∀can␈α∀be␈α∀fixed␈α∪by

␈↓ α∧␈↓introducing␈α
the␈α
notion␈α
of␈α
present␈α
situation.␈α
 An␈α
axiom␈α
that␈α
ostriches␈α
exist␈α
will␈α
do␈α
no␈α
harm␈αif␈α
what

␈↓ α∧␈↓is allowed to vary includes only ostriches that are present.

␈↓ α∧␈↓␈↓ αT4.␈α∂We␈α⊂are␈α∂only␈α⊂part␈α∂way␈α∂to␈α⊂our␈α∂goal␈α⊂of␈α∂providing␈α∂a␈α⊂formalism␈α∂in␈α⊂which␈α∂a␈α⊂database␈α∂of

␈↓ α∧␈↓common␈α
sense␈α
knowledge␈α
can␈αbe␈α
expressed.␈α
 Besides␈α
sets␈α
of␈αaxioms␈α
involving␈α
␈↓↓ab,␈↓␈α
we␈α
need␈αways␈α
of

␈↓ α∧␈↓specifying␈α∂what␈α∂facts␈α∂shall␈α∂be␈α∂taken␈α∂into␈α∞account␈α∂and␈α∂what␈α∂functions␈α∂and␈α∂predicates␈α∂are␈α∂to␈α∞be

␈↓ α∧␈↓taken as variable.

␈↓ α∧␈↓␈↓ αT5.␈α
Non-monotonic␈α∞formalisms␈α
in␈α∞general,␈α
and␈α∞circumscription␈α
in␈α∞particular,␈α
have␈α∞many␈α
as

␈↓ α∧␈↓yet␈α
unrealized␈α
applications␈αto␈α
formalizing␈α
common␈α
sense␈αknowledge␈α
and␈α
reasoning.␈α
 Since␈αwe␈α
have

␈↓ α∧␈↓to␈α
think␈αabout␈α
these␈α
matters␈αin␈α
a␈α
new␈αway,␈α
what␈α
the␈αapplications␈α
are␈α
and␈αhow␈α
to␈α
realize␈αthem␈α
isn't

␈↓ α∧␈↓immediately obvious.  Here are some suggestions.

␈↓ α∧␈↓␈↓ αTWhen␈αwe␈αare␈αsearching␈αfor␈αthe␈α"best"␈αobject␈αof␈αsome␈αkind,␈αwe␈αoften␈αjump␈αto␈αthe␈αconclusion


␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f24


␈↓ α∧␈↓that␈αthe␈αbest␈αwe␈αhave␈αfound␈αso␈αfar␈αis␈αthe␈αbest.␈α This␈αprocess␈αcan␈αbe␈αrepresented␈αas␈αcircumscribing

␈↓ α∧␈↓␈↓↓better(x,candidate),␈↓␈α∪where␈α∪␈↓↓candidate␈↓␈α∪is␈α∩the␈α∪best␈α∪we␈α∪have␈α∪found␈α∩so␈α∪far.␈α∪ If␈α∪we␈α∪attempt␈α∩this

␈↓ α∧␈↓circumscription␈α
while␈αincluding␈α
certain␈α
information␈αin␈α
our␈α
axiom␈α␈↓↓A(better,P),␈↓␈α
where␈α␈↓↓P␈↓␈α
represents

␈↓ α∧␈↓additional␈αpredicates␈αbeing␈αvaried,␈αwe␈αwill␈αsucceed␈αin␈αshowing␈αthat␈αthere␈αis␈αnothing␈αbetter␈αonly␈αif

␈↓ α∧␈↓this␈α
is␈αconsistent␈α
with␈αthe␈α
information␈αwe␈α
take␈αinto␈α
account.␈α If␈α
the␈αattempt␈α
to␈α
circumscribe␈αfails,

␈↓ α∧␈↓we␈α∞would␈α
like␈α∞our␈α
reasoning␈α∞program␈α
to␈α∞use␈α∞the␈α
failure␈α∞as␈α
an␈α∞aid␈α
to␈α∞finding␈α
a␈α∞better␈α∞object.␈α
 I

␈↓ α∧␈↓don't know how hard this would be.



␈↓ α∧␈↓␈↓αAppendix A␈↓

␈↓ α∧␈↓Circumscription in a Proof Checker

␈↓ α∧␈↓␈↓ αTAt␈α
present␈α∞there␈α
are␈α∞no␈α
reasoning␈α∞or␈α
problem-solving␈α∞programs␈α
using␈α∞circumscription.␈α
 A

␈↓ α∧␈↓first␈α
step␈αtowards␈α
such␈αa␈α
program␈α
involves␈αdetermining␈α
what␈αkinds␈α
of␈αreasoning␈α
are␈α
required␈αto

␈↓ α∧␈↓use␈α⊃circumscription␈α⊃effectively.␈α⊃ As␈α∩a␈α⊃step␈α⊃towards␈α⊃this␈α⊃we␈α∩include␈α⊃in␈α⊃this␈α⊃and␈α∩the␈α⊃following

␈↓ α∧␈↓appendix␈αtwo␈α
proofs␈αin␈αEKL␈α
(Ketonen␈αand␈αWeening␈α
1984),␈αan␈αinteractive␈α
theorem␈αprover␈αfor␈α
the

␈↓ α∧␈↓theory␈αof␈αtypes.␈α The␈αfirst␈αdoes␈αthe␈αbird␈αproblem␈αand␈αthe␈αsecond␈αa␈αsimple␈αunique␈αnames␈αproblem.

␈↓ α∧␈↓It␈αwill␈α
be␈αseen␈α
that␈αthe␈αproofs␈α
make␈αsubstantial␈α
use␈αof␈αEKL's␈α
ability␈αto␈α
admit␈αarguments␈αin␈α
second

␈↓ α∧␈↓order logic.

␈↓ α∧␈↓␈↓ αTEach␈αEKL␈αstep␈αbegins␈αwith␈αa␈αcommand␈αgiven␈αby␈αthe␈αuser.␈α This␈αis␈αusually␈αfollowed␈αby␈αthe

␈↓ α∧␈↓sentence␈α
resulting␈αfrom␈α
the␈αstep␈α
in␈αa␈α
group␈αof␈α
lines␈α
each␈αending␈α
in␈αa␈α
semicolon,␈αbut␈α
this␈αis␈α
omitted

␈↓ α∧␈↓for␈α∞definitions␈α∂when␈α∞the␈α∂information␈α∞is␈α∂contained␈α∞in␈α∂the␈α∞command.␈α∂ We␈α∞follow␈α∂each␈α∞step␈α∂by␈α∞a

␈↓ α∧␈↓brief␈αexplanation.␈α Of␈αcourse,␈αthe␈αreader␈αmay␈αskip␈α
this␈αproof␈αif␈αhe␈αis␈αsufficiently␈αclear␈αabout␈α
what

␈↓ α∧␈↓steps␈α∞are␈α∞involved.␈α∞ However,␈α∞I␈α∞found␈α∞that␈α∞pushing␈α∞the␈α∞proof␈α∞through␈α∞EKL␈α∞clarified␈α∂my␈α∞ideas

␈↓ α∧␈↓considerably as well as turning up bugs in my axioms.

␈↓ α∧␈↓ε1. (DEFINE A
␈↓ α∧␈↓ε     |∀AB FLIES.A(AB,FLIES)≡
␈↓ α∧␈↓ε                (∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
␈↓ α∧␈↓ε                (∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f25


␈↓ α∧␈↓ε                (∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
␈↓ α∧␈↓ε                (∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| NIL)
␈↓ α∧␈↓εThis defines the second order predicate ␈↓↓A(ab,flies)␈↓ε, where ␈↓↓ab␈↓ε and
␈↓ α∧␈↓ε␈↓↓flies␈↓ε are predicate variables.  Included here are the specific facts
␈↓ α∧␈↓εabout flying being taken into account.

␈↓ α∧␈↓ε;labels: SIMPINFO
␈↓ α∧␈↓ε2. (AXIOM
␈↓ α∧␈↓ε    |(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧
␈↓ α∧␈↓ε     (∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧
␈↓ α∧␈↓ε     (∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)|)
␈↓ α∧␈↓εThese facts about the distinctness of aspects are used in step 20 only.
␈↓ α∧␈↓εSince axiom 2 is labelled SIMPINFO, the EKL simplifier uses it
␈↓ α∧␈↓εas appropriate when it is asked to simplify a formula.

␈↓ α∧␈↓ε3. (DEFINE A1
␈↓ α∧␈↓ε     |∀AB FLIES.A1(AB,FLIES)≡
␈↓ α∧␈↓ε                A(AB,FLIES)∧
␈↓ α∧␈↓ε                (∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))|
␈↓ α∧␈↓ε     NIL)
␈↓ α∧␈↓εThis is the circumscription formula itself.

␈↓ α∧␈↓ε4. (ASSUME |A1(AB,FLIES)|)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εSince EKL cannot be asked (yet) to do a circumscription, we assume the
␈↓ α∧␈↓εresult.  Most subsequent statements list line 4 as a dependency.
␈↓ α∧␈↓εThis is appropriate since circumscription is a rule of conjecture rather
␈↓ α∧␈↓εthan a rule of inference.

␈↓ α∧␈↓ε5. (DEFINE FLIES2 |∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)| NIL)
␈↓ α∧␈↓εThis definition and the next say what we are going to substitute for
␈↓ α∧␈↓εthe bound predicate variables.

␈↓ α∧␈↓ε6. (DEFINE AB2
␈↓ α∧␈↓ε     |∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))|
␈↓ α∧␈↓εNIL)
␈↓ α∧␈↓εThe fact that this definition is necessarily somewhat awkward makes
␈↓ α∧␈↓εfor some difficulty throughout the proof.

␈↓ α∧␈↓ε7. (RW 4 (OPEN A1))
␈↓ α∧␈↓εA(AB,FLIES)∧(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εThis step merely expands out the circumscription formula.  RW stands
␈↓ α∧␈↓εfor "rewrite a line", in this case line 4.

␈↓ α∧␈↓ε8. (TRW |A(AB,FLIES)| (USE 7))
␈↓ α∧␈↓εA(AB,FLIES)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εWe separate the two conjuncts of 7 in this and the next step.

␈↓ α∧␈↓ε9. (TRW |∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))|
␈↓ α∧␈↓ε(USE 7))
␈↓ α∧␈↓ε∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))
␈↓ α∧␈↓εdeps: (4)

␈↓ α∧␈↓ε10. (RW 8 (OPEN A))␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f26


␈↓ α∧␈↓ε(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
␈↓ α∧␈↓ε(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
␈↓ α∧␈↓ε(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εExpanding out the axiom using the definition ␈↓↓a␈↓ε in step 1.

␈↓ α∧␈↓ε11. (ASSUME |AB2(Z)|)
␈↓ α∧␈↓εdeps: (11)
␈↓ α∧␈↓εOur goal is step 15, but we need to assume its premiss and then
␈↓ α∧␈↓εderive its conclusion.

␈↓ α∧␈↓ε12. (RW 11 (OPEN AB2))
␈↓ α∧␈↓ε(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))
␈↓ α∧␈↓εdeps: (11)
␈↓ α∧␈↓εWe use the definition of ␈↓↓ab2␈↓ε.

␈↓ α∧␈↓ε13. (DERIVE |AB(Z)| (12 10) NIL)
␈↓ α∧␈↓εAB(Z)
␈↓ α∧␈↓εdeps: (4 11)
␈↓ α∧␈↓εThis is our first use of EKL's DERIVE command.  It is based on
␈↓ α∧␈↓εthe notion of direct proof of (Ketonen and Weyhrauch 1984).  Sometimes
␈↓ α∧␈↓εit can do rather complicated things in one step.

␈↓ α∧␈↓ε14. (CI (11) 13 NIL)
␈↓ α∧␈↓εAB2(Z)⊃AB(Z)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εWe discharge the assumption 11 with the "conditional introduction" command.

␈↓ α∧␈↓ε15. (DERIVE |∀Z.AB2(Z)⊃AB(Z)| (14) NIL)
␈↓ α∧␈↓ε∀Z.AB2(Z)⊃AB(Z)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εUniversal generalization.

␈↓ α∧␈↓ε16. (DERIVE
␈↓ α∧␈↓ε      |(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε       (∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧
␈↓ α∧␈↓ε       (∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε       (∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))| () (OPEN AB2 FLIES2))
␈↓ α∧␈↓ε;(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε;(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε;(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
␈↓ α∧␈↓εThis is another rather lengthy computation, but it tells us that ab2 and
␈↓ α∧␈↓εflies2 satisfy the axioms for ab and flies.

␈↓ α∧␈↓ε17. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
␈↓ α∧␈↓ε;A(AB2,FLIES2)≡
␈↓ α∧␈↓ε;(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε;(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε;(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
␈↓ α∧␈↓εNow we substitute ␈↓↓ab2␈↓ε and ␈↓↓flies2␈↓ε in the definition of ␈↓↓A␈↓ε and get
␈↓ α∧␈↓εa result we can compare with step 16.

␈↓ α∧␈↓ε18. (RW 17 (USE 16))
␈↓ α∧␈↓ε;A(AB2,FLIES2)
␈↓ α∧␈↓εWe have shown that ␈↓↓ab2␈↓ε and ␈↓↓flies2␈↓ε satisfy ␈↓↓A.␈↓ε
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f27


␈↓ α∧␈↓ε19. (DERIVE |∀Z.AB(Z)≡AB2(Z)| (9 15 18) NIL)
␈↓ α∧␈↓ε;∀Z.AB(Z)≡AB2(Z)
␈↓ α∧␈↓ε;deps: (4)
␈↓ α∧␈↓ε9 was the circumscription formula, and 15 and 18 are its two premisses,
␈↓ α∧␈↓εso we can now derive its conclusion.  Now we know exactly what entities
␈↓ α∧␈↓εare abnormal.

␈↓ α∧␈↓ε20. (RW 8 ((USE 1 MODE: EXACT) ((USE 19 MODE: EXACT) (OPEN AB2))))
␈↓ α∧␈↓ε;(∀X.¬(∃X1.BIRD(X1)∧X=X1)⊃¬FLIES(X))∧
␈↓ α∧␈↓ε;(∀X.BIRD(X)∧¬(∃X2.OSTRICH(X2)∧X=X2)⊃FLIES(X))∧(∀X.OSTRICH(X)⊃¬FLIES(X))
␈↓ α∧␈↓ε;deps: (4)
␈↓ α∧␈↓εWe rewrite the axiom now that we know what's abnormal.  This gives
␈↓ α∧␈↓εa somewhat awkward formula that nevertheless contains the desired
␈↓ α∧␈↓εconclusion.  The occurrences of equality are left over from the
␈↓ α∧␈↓εelimination of the aspects that used the axiom of step 2.

␈↓ α∧␈↓ε21. (DERIVE |∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)| (20) NIL)
␈↓ α∧␈↓ε;∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)
␈↓ α∧␈↓ε;deps: (4)
␈↓ α∧␈↓εDERIVE straightens out 20 to put the conclusion in the desired form.
␈↓ α∧␈↓εThe result is still dependent on the assumption of the correctness of
␈↓ α∧␈↓εthe circumscription made in step 4.

␈↓ α∧␈↓␈↓ αTClearly if circumscription is to become a practical technique,
␈↓ α∧␈↓the reasoning has to become much more automatic.



␈↓ α∧␈↓␈↓αAppendix B␈↓

␈↓ α∧␈↓␈↓ αTHere␈αis␈αan␈α
annotated␈αEKL␈αproof␈α
that␈αcircumscribes␈αthe␈α
predicate␈α␈↓↓e(x,y)␈↓␈αdiscussed␈αin␈α
section

␈↓ α∧␈↓6.

␈↓ α∧␈↓ε(proof unique names)
␈↓ α∧␈↓εWhat the user types is indicated by the numbered statements in lower
␈↓ α∧␈↓εcase.  What EKL types is preceded by semicolons at the beginning of
␈↓ α∧␈↓εeach line and is in upper case.  We omit EKL's type-out when it merely
␈↓ α∧␈↓εrepeats what the command asked it to do, as in the commands  DERIVE,
␈↓ α∧␈↓εASSUME  and DEFINE.

␈↓ α∧␈↓ε1. (axiom |index a = 1 ∧ index b = 2 ∧ index c = 3 ∧ index d = 4|)
␈↓ α∧␈↓εSince EKL does not have attachments to determine the equivalence of names,
␈↓ α∧␈↓εwe establish a correspondence between the names in our domain and some
␈↓ α∧␈↓εnatural numbers.

␈↓ α∧␈↓ε2. (derive |¬(1=2) ∧ ¬(1=3) ∧ ¬(2=3) ∧ ¬(1=4) ∧ ¬(2=4) ∧ ¬(2=4)|)
␈↓ α∧␈↓εEKL does know about the distinctness of natural numbers, so this
␈↓ α∧␈↓εcan be derived.

␈↓ α∧␈↓ε(der-slow)
␈↓ α∧␈↓εWe have to tell EKL to use the properties of equality rather than
␈↓ α∧␈↓εregarding it as just another predicate symbol in order to do the next
␈↓ α∧␈↓εstep.  Sometimes this leads to combinatorial explosion.
␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f28


␈↓ α∧␈↓ε3. (derive |a ≠ b| (1 2))
␈↓ α∧␈↓εThis shows that two names themselves are distinct.

␈↓ α∧␈↓ε4. (define equiv |∀e.equiv e ≡ (∀x.e(x,x)) ∧ (∀x y.e(x,y) ⊃ e(y,x))
␈↓ α∧␈↓ε␈↓ αT∧ (∀x y z.e(x,y) ∧ e(y,z) ⊃ e(x,z))|)
␈↓ α∧␈↓εHere we use second order logic to define the notion of equivalence
␈↓ α∧␈↓εrelation.  The first word after "define" is the entity being defined
␈↓ α∧␈↓εand included between vertical bars is the defining relation.  EKL
␈↓ α∧␈↓εchecks that an entity satisfying the relation exists.

␈↓ α∧␈↓ε5. (define ax |∀e.ax e ≡ e(a,b) ∧ equiv e|)
␈↓ α∧␈↓εWe define  ax  as a predicate we want our imitation equality to
␈↓ α∧␈↓εsatisfy.  We have chosen a very simple case, namely making  a  and
␈↓ α∧␈↓εb  "equal" and nothing else.

␈↓ α∧␈↓ε6. (define ax1 |∀e.ax1 e ≡ ax e ∧ ∀e1.(ax e1 ∧ (∀x y.e1(x,y) ⊃ e(x,y))
␈↓ α∧␈↓ε␈↓ αT⊃ (∀x y.e(x,y) ≡ e1(x,y)))|)
␈↓ α∧␈↓εThis defines  ax1  as the second order predicate specifying the
␈↓ α∧␈↓εcircumscription of  ax.

␈↓ α∧␈↓ε7. (assume |ax1(e0)|)
␈↓ α∧␈↓ε(label circum)
␈↓ α∧␈↓εWe now specify that  e0  satisfies  ax1.  It takes till step 17
␈↓ α∧␈↓εto determine what  e0  actually is.  When EKL includes circumscription
␈↓ α∧␈↓εas an operator, we may be able to write something like  circumscribe(e0,ax1)
␈↓ α∧␈↓εand make this step occur.  For now it's just an ordinary assumption.

␈↓ α∧␈↓ε8. (define e2 |∀x y.e2(x,y) ≡ (x = a ∧ y = b) ∨ (x = b ∧ y = a) ∨ x = y|)
␈↓ α∧␈↓εThe predicate  e2  defined here is what  e0  will turn out to be.

λ∂↓ α∧␈↓ε9. (derive |equiv e2| nil (open equiv) (open e2))
␈↓ α∧␈↓εNow EKL agrees that  e2  is an equivalence relation.  This step takes
␈↓ α∧␈↓εthe KL-10 about 14 seconds.

␈↓ α∧␈↓ε10. (derive |ax e2| (9) (open ax) (open e2))
␈↓ α∧␈↓ε(label ax e2)
␈↓ α∧␈↓εMoreover it satisfies  ax.

␈↓ α∧␈↓ε11. (rw circum (open ax1))
␈↓ α∧␈↓ε;AX(E0)∧(∀E1.AX(E1)∧(∀X Y.E1(X,Y)⊃E0(X,Y))⊃(∀X Y.E0(X,Y)≡E1(X,Y)))
␈↓ α∧␈↓ε;deps: (CIRCUM)
␈↓ α∧␈↓εA trivial step of expanding the definition of  ax1.  EKL tells us
␈↓ α∧␈↓εthat this fact depends on the assumption CIRCUM.  So do many of
␈↓ α∧␈↓εthe subsequent lines of the proof, but we omit it henceforth to
␈↓ α∧␈↓εsave space.

␈↓ α∧␈↓ε12. (trw |ax e0| (use 11))
␈↓ α∧␈↓ε;AX(E0)
␈↓ α∧␈↓εThe first conjunct of the previous step.

␈↓ α∧␈↓ε13. (rw 12 (open ax equiv))
␈↓ α∧␈↓ε(label fact1)
␈↓ α∧␈↓ε;E0(A,B)∧(∀X.E0(X,X))∧(∀X Y.E0(X,Y)⊃E0(Y,X))∧(∀X Y Z.E0(X,Y)∧E0(Y,Z)⊃E0(X,Z))
␈↓ α∧␈↓εWe expand  ax e0  according to the definitions of  ax  and  equiv.

␈↓ α∧␈↓ε14. (derive |∀p q r.(p ∨ q ⊃ r) ≡ (p ⊃ r) ∧ (q ⊃ r)|)␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f29


␈↓ α∧␈↓ε(label rewrite by cases)
␈↓ α∧␈↓εThis is a fact of propositional calculus used as a rewrite rule in the
␈↓ α∧␈↓εnext step.  A program that can use circumscription by itself will either
␈↓ α∧␈↓εneed to generate this step or systematically avoid the need for it.

␈↓ α∧␈↓ε15. (trw |e2(x,y) ⊃ e0(x,y)|
␈↓ α∧␈↓ε      ((open e2) (use rewrite by cases mode: always) (use fact1)))
␈↓ α∧␈↓ε;E2(X,Y)⊃E0(X,Y)
␈↓ α∧␈↓εThis is the least obvious step, because  rewrite by cases is used
␈↓ α∧␈↓εafter some preliminary transformation of the formula.

␈↓ α∧␈↓ε16. (derive |∀x y.e0(x,y) ≡ e2(x,y)| (ax e2 11 15))
␈↓ α∧␈↓εDERIVE is subsituting  e2  for the variable  e1 in step 11 and using
␈↓ α∧␈↓εthe fact  ax(e2)  and step 15 to infer the conclusion of the implication
␈↓ α∧␈↓εthat follows the quantifier ∀e.

␈↓ α∧␈↓ε17. (rw 16 (open E2))
␈↓ α∧␈↓ε;∀X Y.E0(X,Y)≡X=A∧Y=B∨X=B∧Y=A∨X=Y
␈↓ α∧␈↓ε;deps: (CIRCUM)
␈↓ α∧␈↓εExpanding the definition of  e2  tells us the final result of circumscribing
␈↓ α∧␈↓εe0(x,y).  A more complex  ax(e0) - see step 5 - would give a more complex
␈↓ α∧␈↓εresult upon circumscription.  However, it seems that the proof would be
␈↓ α∧␈↓εsimilar.  Therefore, it could perhaps be made into some kind of macro.



␈↓ α∧␈↓13. ␈↓αAcknowledgments␈↓

␈↓ α∧␈↓␈↓ αTI␈α
have␈α
had␈α
useful␈α
discussions␈α
with␈α
Matthew␈α
Ginsberg,␈α
Benjamin␈α
Grosof,␈αVladimir␈α
Lifschitz

␈↓ α∧␈↓and␈αLeslie␈αPack.␈α The␈αwork␈αwas␈αpartially␈αsupported␈αby␈αNSF␈αand␈αby␈αDARPA.␈α I␈αalso␈αthank␈αJussi

␈↓ α∧␈↓Ketonen␈αfor␈αdeveloping␈αEKL␈αand␈αhelping␈αme␈αwith␈αits␈αuse.␈α In␈αparticular␈αhe␈αgreatly␈αshortened␈αthe

␈↓ α∧␈↓unique names proof.


␈↓ α∧␈↓14. ␈↓αReferences:␈↓

␈↓ α∧␈↓␈↓αEtherington,␈α→David␈α→W.␈α→and␈α→Raymond␈α→Reiter␈α→(1983)␈↓:␈α→"On␈α→Inheritance␈α~Hierarchies␈α→with
␈↓ α∧␈↓Exceptions",␈α∀in␈α∀␈↓↓Proceedings␈α∀of␈α∀the␈α∀National␈α∀Conference␈α∀on␈α∀Artificial␈α∀Intelligence,␈α∀AAAI-83␈↓,
␈↓ α∧␈↓William Kaufman, Inc.

␈↓ α∧␈↓␈↓αKetonen,␈α⊂Jussi␈α⊃and␈α⊂Joseph␈α⊂S.␈α⊃Weening␈α⊂(1984)␈↓:␈α⊃␈↓↓EKL␈α⊂-␈α⊂An␈α⊃Interactive␈α⊂Proof␈α⊃Checker,␈α⊂User's
␈↓ α∧␈↓↓Reference Manual␈↓, Computer Science Department, Stanford University.

␈↓ α∧␈↓␈↓αKetonen,␈α⊗Jussi␈α⊗and␈α⊗Richard␈α⊗W.␈α∃Weyhrauch␈α⊗(1984)␈↓:␈α⊗"A␈α⊗Decidable␈α⊗Fragment␈α⊗of␈α∃Predicate
␈↓ α∧␈↓Calculus", accepted for publication in the ␈↓↓Journal for Theoretical Computer Science␈↓.

␈↓ α∧␈↓␈↓αLifschitz, Vladimir␈↓(1983): unpublished note on circumscription.

␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧
␈↓ α∧␈↓July 16, 1984␈↓ ¬4Applications of Circumscription␈↓ f30


␈↓ α∧␈↓␈↓αMcCarthy,␈α∂John␈α∂and␈α∞P.J.␈α∂Hayes␈α∂(1969)␈↓:␈α∞"Some␈α∂Philosophical␈α∂Problems␈α∞from␈α∂the␈α∂Standpoint␈α∞of
␈↓ α∧␈↓Artificial␈α
Intelligence",␈α∞in␈α
D.␈α
Michie␈α∞(ed),␈α
␈↓↓Machine␈α
Intelligence␈α∞4␈↓,␈α
American␈α
Elsevier,␈α∞New␈α
York,
␈↓ α∧␈↓NY.

␈↓ α∧␈↓␈↓αMcCarthy,␈α∂John␈α∂(1977)␈↓:␈α∂"Epistemological␈α∂Problems␈α∂of␈α∂Artificial␈α∂Intelligence",␈α∂␈↓↓Proceedings␈α∂of␈α∞the
␈↓ α∧␈↓↓Fifth International Joint Conference on Artificial Intelligence␈↓, M.I.T., Cambridge, Mass.

␈↓ α∧␈↓␈↓αMcCarthy,␈α∪John␈α∩(1979)␈↓:␈α∪"First␈α∩Order␈α∪Theories␈α∩of␈α∪Individual␈α∩Concepts␈α∪and␈α∪Propositions",␈α∩in
␈↓ α∧␈↓Michie, Donald (ed.) ␈↓↓Machine Intelligence 9␈↓, (University of Edinburgh Press, Edinburgh).

␈↓ α∧␈↓␈↓αMcCarthy,␈α⊃John␈α⊃(1980)␈↓:␈α⊃"Circumscription␈α∩-␈α⊃A␈α⊃Form␈α⊃of␈α⊃Non-Monotonic␈α∩Reasoning",␈α⊃␈↓↓Artificial
␈↓ α∧␈↓↓Intelligence␈↓, Volume 13, Numbers 1,2, April.

␈↓ α∧␈↓␈↓αMinsky,␈α
Marvin␈α
(1982)␈↓:␈α
in␈α
various␈α
lectures␈α
including␈α
AAAI␈α
Presidential␈α
Address␈α
though␈α
not␈αin␈α
its
␈↓ α∧␈↓written form.

␈↓ α∧␈↓␈↓αReiter,␈α⊃Raymond␈α⊃(1980)␈↓:␈α⊃"A␈α⊃Logic␈α⊃for␈α⊃Default␈α⊃Reasoning",␈α⊃␈↓↓Artificial␈α⊃Intelligence␈↓,␈α⊃Volume␈α⊂13,
␈↓ α∧␈↓Numbers 1,2, April.

␈↓ α∧␈↓␈↓αReiter,␈α
Raymond␈α∞(1980b)␈↓:␈α
"Equality␈α
and␈α∞domain␈α
closure␈α
in␈α∞first␈α
order␈α
data␈α∞bases",␈α
J.␈α∞ACM,␈α
27,
␈↓ α∧␈↓Apr. 1980, 235-249.

␈↓ α∧␈↓␈↓αReiter,␈α!Raymond␈α!(1982)␈↓:␈α""Circumscription␈α!Implies␈α!Predicate␈α"Completion␈α!(Sometimes)",
␈↓ α∧␈↓Proceedings of the National Conference on Artificial Intelligence, AAAI-82.

























␈↓ α∧␈↓␈↓ ¬IJUST ANOTHER DRAFT␈↓ ∧